English
If c1 is related to c2 by LiftRel (LiftRel R), then flatten c1 and flatten c2 are related by LiftRel R.
Русский
Если c1 связано с c2 отношением LiftRel (LiftRel R), то flatten c1 и flatten c2 связаны отношением LiftRel R.
LaTeX
$$$$\mathrm{LiftRel}(\mathrm{LiftRel}(R))\ c1\ c2 \Rightarrow \mathrm{LiftRel}\ R\ (\mathrm{flatten}(c1))\ (\mathrm{flatten}(c2)).$$$$
Lean4
theorem liftRel_flatten {R : α → β → Prop} {c1 : Computation (WSeq α)} {c2 : Computation (WSeq β)}
(h : c1.LiftRel (LiftRel R) c2) : LiftRel R (flatten c1) (flatten c2) :=
let S s t := ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
⟨S, ⟨c1, c2, rfl, rfl, h⟩, fun {s t} h =>
match s, t, h with
| _, _, ⟨c1, c2, rfl, rfl, h⟩ => by
simp only [destruct_flatten]; apply liftRel_bind _ _ h
intro a b ab; apply Computation.LiftRel.imp _ _ _ (liftRel_destruct ab)
intro a b; apply LiftRelO.imp_right
intro s t h; refine ⟨Computation.pure s, Computation.pure t, ?_, ?_, ?_⟩ <;> simp [h]⟩
