Right leads To out

theorem right_leadsTo_out (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 | ⟨p, inr (inp ⟨0, npos⟩)⟩ ∈ s.msgs}      {s | (s.proc p).out = some (inp ⟨0, npos⟩)} := by  let m : Message (Fin n) M := ⟨p, inr (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 p, 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]  grind [inv_tr_right npos inp hj htr]