English
If h1 relates s1 and s2 by R and h2 relates f1 a and f2 b whenever R a b, then LiftRel S holds between bind s1 f1 and bind s2 f2.
Русский
Если h1 связывает s1 и s2 по R, а h2 связывает f1 a и f2 b при R a b, то LiftRel S держится между связкой bind s1 f1 и bind s2 f2.
LaTeX
$$$\\text{LiftRel }S(\\text{bind } s1\\ f1)(\\text{bind } s2\\ f2)\\ \n\\text{при}\\ h1:\\ \\mathrm{LiftRel }R s1 s2\\ \\text{и}\\ h2:\\ \\forall a b, R\\ a\\ b \\rightarrow \\mathrm{LiftRel }S (f1\\ a)(f2\\ b)$$$
Lean4
theorem liftRel_bind {δ} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α} {s2 : Computation β}
{f1 : α → Computation γ} {f2 : β → Computation δ} (h1 : LiftRel R s1 s2)
(h2 : ∀ {a b}, R a b → LiftRel S (f1 a) (f2 b)) : LiftRel S (bind s1 f1) (bind s2 f2) :=
let ⟨l1, r1⟩ := h1
⟨fun {_} cB =>
let ⟨_, a1, c₁⟩ := exists_of_mem_bind cB
let ⟨_, b2, ab⟩ := l1 a1
let ⟨l2, _⟩ := h2 ab
let ⟨_, d2, cd⟩ := l2 c₁
⟨_, mem_bind b2 d2, cd⟩,
fun {_} dB =>
let ⟨_, b1, d1⟩ := exists_of_mem_bind dB
let ⟨_, a2, ab⟩ := r1 b1
let ⟨_, r2⟩ := h2 ab
let ⟨_, c₂, cd⟩ := r2 d1
⟨_, mem_bind a2 c₂, cd⟩⟩
