Left leads To right

theorem left_leadsTo_right (inp : Fin n → Bool)    {ss : ωSequence (State (Fin n) M S)} {xs : ωSequence (Action (Fin n) M)}    (ha : (alg npos).AdmissibleRun inp 0 ss xs) (p : Fin n) :    ss.LeadsTo {s | ⟨⟨0, npos⟩, inl (inp ⟨0, npos⟩)⟩ ∈ s.msgs}      {s | ⟨p, inr (inp ⟨0, npos⟩)⟩ ∈ s.msgs} := by  let m : Message (Fin n) M := ⟨⟨0, npos⟩, inl (inp ⟨0, npos⟩)⟩  intro k _  have : m ∈ (ss k).msgs := by grind  obtain ⟨_, _, hf⟩ := AdmissibleRun.fault_zero.mp ha  obtain ⟨j, _, _⟩ : ∃ j, k ≤ j ∧ xs j = some m := by grind [hf ⟨0, npos⟩, ProcFair]  use j + 1  have hj := always_inv npos inp ha j  have htr : (alg npos).lts.Tr (ss j) (some m) (ss (j + 1)) := by grind [LTS.OmegaExecution]  have h1 : k ≤ j + 1 := by grind  simp [h1, m, inv_tr_left npos inp hj htr rfl]