English
If LiftRel R s t holds, then the Destructs of s and t satisfy Computation.LiftRel with LiftRelO R (LiftRel R).
Русский
Если выполняется LiftRel R s t, то Destruct s и Destruct t удовлетворяют Computation.LiftRel с LiftRelO R (LiftRel R).
LaTeX
$$$$ \mathrm{LiftRel}\ R\ s\ t \Rightarrow \mathrm{Computation.LiftRel}\ (\mathrm{LiftRelO}\ R (\mathrm{LiftRel R}))\ (\mathrm{destruct}\ s)\ (\mathrm{destruct}\ t). $$$$
Lean4
theorem liftRel_destruct {R : α → β → Prop} {s : WSeq α} {t : WSeq β} :
LiftRel R s t → Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
| ⟨R, h1, h2⟩ => by
refine Computation.LiftRel.imp ?_ _ _ (h2 h1)
apply LiftRelO.imp_right
exact fun s' t' h' => ⟨R, h', @h2⟩
