English
A standard coinduction principle for Seq: if head(s1) = head(s2) and any fr preserving equality for all β, fr, implies fr(tail(s1)) = fr(tail(s2)), then s1 = s2.
Русский
Стандартный принцип когоиндукции для Seq: если головы совпадают и для всех β и функций fr, сохраняющих равенство, выполняется fr(хвост) равняется, то последовательности равны.
LaTeX
$$$\\text{coinduction} : \\forall s_1 s_2,\\; head(s_1) = head(s_2) \\rightarrow (\\forall \\beta (fr : Seq\\ α \\to \\beta),\\; fr(s_1) = fr(s_2) \\rightarrow fr(tail(s_1)) = fr(tail(s_2))) \\rightarrow s_1 = s_2$$$
Lean4
theorem coinduction :
∀ {s₁ s₂ : Seq α},
head s₁ = head s₂ → (∀ (β : Type u) (fr : Seq α → β), fr s₁ = fr s₂ → fr (tail s₁) = fr (tail s₂)) → s₁ = s₂
| _, _, hh, ht => Subtype.eq (Stream'.coinduction hh fun β fr => ht β fun s => fr s.1)
