destruct_cons — Mathlib

English

If destruct s equals some (a, s'), then s equals cons a s'.

Русский

Если destruct s равно some (a, s'), тогда s = cons a s'.

LaTeX

$$$\\forall {\\alpha} {s:\\mathrm{Seq}\\alpha} {a:\\alpha} {s':\\mathrm{Seq}\\alpha},\\; \\mathrm{destruct}\\ s = \\mathrm{some}\\ (a,s') \\Rightarrow s = \\mathrm{cons}\\ a\\ s'.$$$

Lean4

@[simp]
theorem destruct_cons (a : α) : ∀ s, destruct (cons a s) = some (a, s)
  | ⟨f, al⟩ => by
    unfold cons destruct Functor.map
    apply congr_arg fun s => some (a, s)
    apply Subtype.eq; dsimp [tail]

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