English
LiftRel R s t is equivalent to Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t).
Русский
LiftRel R s t эквивалентно Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t).
LaTeX
$$$$ \LiftRel R s t \iff \mathrm{Computation.LiftRel}\ (\mathrm{LiftRelO}\ R (\mathrm{LiftRel R}))\ (\mathrm{destruct}\ s)\ (\mathrm{destruct}\ t). $$$$
Lean4
theorem liftRel_destruct_iff {R : α → β → Prop} {s : WSeq α} {t : WSeq β} :
LiftRel R s t ↔ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t) :=
⟨liftRel_destruct, fun h =>
⟨fun s t => LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t), Or.inr h,
fun {s t} h =>
by
have h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t) :=
by
obtain h | h := h
· exact liftRel_destruct h
· assumption
apply Computation.LiftRel.imp _ _ _ h
intro a b
apply LiftRelO.imp_right
intro s t
apply Or.inl⟩⟩
