English
If R is a bisimulation on M P and h provides a witness that every related pair can be decomposed into matching heads with children remaining related, then for all x,y with R x y, x = y. This is a direct lift of the previous extensional principle to a general bisimulation setting.
Русский
Если R — бисимуляция на M P и дано доказательство того, что каждую пару связанных элементов можно разложить на совпадающие головы и связанные дети сохраняют отношение, то для любых x,y с R x y выполняется x = y. Это естественное обобщение предыдущей экстенсиональности для бисимуляции.
LaTeX
$$$\forall R,\; (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)) \Rightarrow ∀ x y, R x y → x = y$$$
Lean4
theorem bisim (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 := by
introv h'
haveI := Inhabited.mk x.head
apply eq_of_bisim R _ _ _ h'; clear h' x y
constructor <;> introv ih <;> rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩ <;> clear h
· replace h₀ := congr_arg Sigma.fst h₀
replace h₁ := congr_arg Sigma.fst h₁
simp only [dest_mk] at h₀ h₁
rw [h₀, h₁]
· simp only [dest_mk] at h₀ h₁
cases h₀
cases h₁
apply h₂
