English
If R is a bisimulation on M P and h provides a compatible witness, then for any x,y with R x y, x = y. This is a direct consequence of the bisimulation lifting to equality.
Русский
Если R — бисимуляция на M P и существует совместимый свидетель, то для любых x,y с R x y выполняется x = y. Это следствие из бисимуляции, разрешающей переход к равенству.
LaTeX
$$$\forall {P},{R}, (bisim : IsBisimulation R) \to (\forall x y, R x y → x = y)$$$
Lean4
theorem bisim_equiv (R : M P → M P → Prop)
(h : ∀ x y, R x y → ∃ a f f', M.dest x = ⟨a, f⟩ ∧ M.dest y = ⟨a, f'⟩ ∧ ∀ i, R (f i) (f' i)) :
∀ x y, R x y → x = y := fun x y Rxy =>
let Q : M P × M P → Prop := fun p => R p.fst p.snd
bisim' Q Prod.fst Prod.snd
(fun p Qp =>
let ⟨a, f, f', hx, hy, h'⟩ := h p.fst p.snd Qp
⟨a, f, f', hx, hy, fun i => ⟨⟨f i, f' i⟩, h' i, rfl, rfl⟩⟩)
⟨x, y⟩ Rxy
