English
The reverseRecOn of a concatenation xs ++ [x] relates to reverseRecOn xs by applying the constructor to x and xs.
Русский
Обратное рекурсивное свёртывание для xs ++ [x] связано с reverseRecOn xs через конструктор, добавляющий x.
LaTeX
$$$$ \operatorname{reverseRecOn} (xs ++ [x]) \; nil \; append\_singleton = append\_singleton\; xs\; x\; (\operatorname{reverseRecOn} xs \; nil \; append\_singleton). $$$$
Lean4
@[simp, nolint unusedHavesSuffices]
theorem reverseRecOn_concat {motive : List α → Sort*} (x : α) (xs : List α) (nil : motive [])
(append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) :
reverseRecOn (motive := motive) (xs ++ [x]) nil append_singleton =
append_singleton _ _ (reverseRecOn (motive := motive) xs nil append_singleton) :=
by grind [reverseRecOn]
