cons_eq_cons — Mathlib

English

Equality of cons terms is equivalent to equality of heads and tails.

Русский

Сравнение cons поэлементно эквивалентно равенству головых и хвостов.

LaTeX

$$$(\\mathrm{cons}\\ x\\ s = \\mathrm{cons}\\ x'\\ s') \\iff (x=x' \\land s=s').$$$

Lean4

theorem cons_eq_cons {x x' : α} {s s' : Seq α} : (cons x s = cons x' s') ↔ (x = x' ∧ s = s') :=
  by
  constructor
  · apply cons_injective2
  · intro ⟨_, _⟩
    congr

Похожие утверждения