English
If xs is nonempty, recNeNil applied to (x :: xs) reduces to cons x xs h of the tail and recNeNil of xs.
Русский
Если xs непуст, то recNeNil для (x :: xs) сводится к cons x xs h и рекурсивному вызову recNeNil для xs.
LaTeX
$$$$ \operatorname{recNeNil} (\text{singleton}) (\text{cons}) (x :: xs) (\text{cons\_ne\_nil } x xs) = \text{cons } x\, xs\, h\, (\operatorname{recNeNil} (\text{singleton}) (\text{cons}) xs h). $$$$
Lean4
@[simp]
theorem recNeNil_cons {motive : (l : List α) → l ≠ [] → Sort*} (x : α) (xs : List α) (h : xs ≠ [])
(singleton : ∀ x, motive [x] (cons_ne_nil x []))
(cons : ∀ x xs h, motive xs h → motive (x :: xs) (cons_ne_nil x xs)) :
recNeNil singleton cons (x :: xs) (cons_ne_nil x xs) = cons x xs h (recNeNil singleton cons xs h) :=
match xs with
| _ :: _ => rfl
