English
The value of bidirectionalRec on a cons-append structure a :: (l ++ [b]) is determined by the cons-append rule applied to the tail.
Русский
Значение bidirectionalRec для структуры a :: (l ++ [b]) определяется правилом cons-append применительно к хвосту.
LaTeX
$$$$ \operatorname{bidirectionalRec} (\text{nil}) (\text{singleton}) (\text{cons\_append}) (a :: (l ++ [b])) = \text{cons\_append } a\, l\, b\; (\operatorname{bidirectionalRec} (\text{nil}) (\text{singleton}) (\text{cons\_append}) l). $$$$
Lean4
@[simp]
theorem bidirectionalRec_singleton {motive : List α → Sort*} (nil : motive []) (singleton : ∀ a : α, motive [a])
(cons_append : ∀ (a : α) (l : List α) (b : α), motive l → motive (a :: (l ++ [b]))) (a : α) :
bidirectionalRec nil singleton cons_append [a] = singleton a := by simp [bidirectionalRec]
