reverseRecOn_nil — Mathlib

English

The recursive reverse on an empty list yields the base motive value.

Русский

Рекурсивное обращение списка по пустому списку даёт базовое значение мотива.

LaTeX

$$$$ \operatorname{reverseRecOn} (\text{motive}) ([]) = nil. $$$$

Lean4

@[simp]
theorem reverseRecOn_nil {motive : List α → Sort*} (nil : motive [])
    (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) :
    reverseRecOn [] nil append_singleton = nil :=
  reverseRecOn.eq_1 ..
    -- `unusedHavesSuffices` is getting confused by the unfolding of `reverseRecOn`

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