English
For any lists l1, l2 and any element a, the last element obtained from l1 ++ (a :: l2) is the same as the last element from a :: l2.
Русский
Для любых списков l1, l2 и элемента a последнее значение у списка l1 ++ (a :: l2) совпадает с последним значением у a :: l2.
LaTeX
$$$\forall l_1:\, List\;\alpha\,\; a:\, \alpha\,\; l_2:\, List\;\alpha,\;\; \mathrm{getLast?}(l_1 ++ a :: l_2) = \mathrm{getLast?}(a :: l_2)$$$
Lean4
theorem getLast?_append_cons : ∀ (l₁ : List α) (a : α) (l₂ : List α), getLast? (l₁ ++ a :: l₂) = getLast? (a :: l₂)
| [], _, _ => rfl
| [_], _, _ => rfl
| b :: c :: l₁, a, l₂ => by
rw [cons_append, cons_append, getLast?_cons_cons, ← cons_append, getLast?_append_cons (c :: l₁)]
