Lean4
theorem coinduction {s₁ s₂ : Stream' α} :
head s₁ = head s₂ → (∀ (β : Type u) (fr : Stream' α → β), fr s₁ = fr s₂ → fr (tail s₁) = fr (tail s₂)) → s₁ = s₂ :=
fun hh ht =>
eq_of_bisim
(fun s₁ s₂ => head s₁ = head s₂ ∧ ∀ (β : Type u) (fr : Stream' α → β), fr s₁ = fr s₂ → fr (tail s₁) = fr (tail s₂))
(fun s₁ s₂ h =>
have h₁ : head s₁ = head s₂ := And.left h
have h₂ : head (tail s₁) = head (tail s₂) := And.right h α (@head α) h₁
have h₃ :
∀ (β : Type u) (fr : Stream' α → β), fr (tail s₁) = fr (tail s₂) → fr (tail (tail s₁)) = fr (tail (tail s₂)) :=
fun β fr => And.right h β fun s => fr (tail s)
And.intro h₁ (And.intro h₂ h₃))
(And.intro hh ht)
