English
If ca ≈ ca' and cb ≈ cb' (equivalences), then LiftRel R ca cb is equivalent to LiftRel R ca' cb'.
Русский
Если ca эквивалентно ca' и cb эквивалентно cb', то LiftRel R ca cb эквивалентно LiftRel R ca' cb'.
LaTeX
$$$\\ca \\\\approx \\\\ca' \\Rightarrow \\cb \\\\approx \\\\cb' \\Rightarrow \\mathrm{LiftRel}\\,R\\ ca\\ cb \\iff \\mathrm{LiftRel}\\,R\\ ca'\\ cb'$$$
Lean4
theorem liftRel_congr {R : α → β → Prop} {ca ca' : Computation α} {cb cb' : Computation β} (ha : ca ~ ca')
(hb : cb ~ cb') : LiftRel R ca cb ↔ LiftRel R ca' cb' :=
and_congr (forall_congr' fun _ => imp_congr (ha _) <| exists_congr fun _ => and_congr (hb _) Iff.rfl)
(forall_congr' fun _ => imp_congr (hb _) <| exists_congr fun _ => and_congr (ha _) Iff.rfl)
