English
Let l be a list and n a natural number with n < length(l). Then l[n] :: l.drop (n+1) = l.drop n, i.e. the head at position n consed onto the tail after dropping the next element equals the drop at n.
Русский
Пусть l — список и n — натуральное число, удовлетворяющее n < |l|. Тогда l[n] :: l.drop (n+1) = l.drop n, т.е. голова на позиции n конструирует хвост после пропуска следующего элемента и равна отбрасыванию первых n элементов.
LaTeX
$$$\\forall \\{l : List\\,\\alpha\\}, \\forall n, n < |l| \\;\\Rightarrow\\; l[n] :: l.drop (n+1) = l.drop n$$$
Lean4
theorem cons_getElem_drop_succ {l : List α} {n : Nat} {h : n < l.length} : l[n] :: l.drop (n + 1) = l.drop n :=
(drop_eq_getElem_cons h).symm
