English
The same recursion rule as above holds, expressed with a cast in a more detailed form.
Русский
Та же рекурсивная формула, но с явной вставкой приведения в более детальной форме.
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_cons_append {motive : List α → Sort*} (nil : motive []) (singleton : ∀ a : α, motive [a])
(cons_append : ∀ (a : α) (l : List α) (b : α), motive l → motive (a :: (l ++ [b]))) (a : α) (l : List α) (b : α) :
bidirectionalRec nil singleton cons_append (a :: (l ++ [b])) =
cons_append a l b (bidirectionalRec nil singleton cons_append l) :=
by
conv_lhs => unfold bidirectionalRec
cases l with grind
