English
Enumerating a sequence built by cons x s yields the first element (0, x) and the rest obtained by incrementing indices in the enumeration of s.
Русский
Перечисление последовательности, построенной как cons x s, даёт первую пару (0, x) и остальное через инкремент индексов в перечислении s.
LaTeX
$$$$ \\mathrm{enum}(\\mathrm{cons}\\ x\\ s) = \\mathrm{cons}(0,x)\\ (\\mathrm{map}(\\mathrm{Prod.map}(\\mathrm{Nat.succ}, \\mathrm{id}))\\ (\\mathrm{enum}\\ s)). $$$$
Lean4
@[simp]
theorem enum_cons (s : Seq α) (x : α) : enum (cons x s) = cons (0, x) (map (Prod.map Nat.succ id) (enum s)) :=
by
ext ⟨n⟩ : 1
· simp
· simp only [get?_enum, get?_cons_succ, map_get?, Option.map_map]
congr
