English
Let α be a type with decidable equality, and l a list of α. For any y, z ∈ α and x ∈ α, if x ∈ y :: z :: l and x ≠ y and x ≠ z, then the predecessor of x in the list y :: z :: l equals the predecessor of x in the tail z :: l (with the obvious witness that x ∈ z :: l).
Русский
Пусть α - множество с разрешённым равенством; l — список элементов α. Пусть y, z ∈ α и x ∈ α. Если x принадлежит списку y, z, l в виде y :: z :: l и x ≠ y, x ≠ z, то предшественник x в списке y :: z :: l совпадает с предшественником x в хвосте z :: l (при соответствующем доказательстве x ∈ z :: l).
LaTeX
$$$\forall \alpha \ (A:\text{Type}) [DecidableEq\ A]\quad \forall l:A\to\text{List}\ A,\ \forall x,y,z:A,\\
\ h:x\in y::z::l, \ hy: x\neq y, \ hz: x\neq z\ \Rightarrow\ prev(y::z::l)\ x\ h = prev(z::l)\ x\ (by\ simpa[hy] using h).$$$
Lean4
theorem prev_ne_cons_cons (y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz : x ≠ z) :
prev (y :: z :: l) x h = prev (z :: l) x (by simpa [hy] using h) :=
by
cases l
· simp [hy, hz] at h
· rw [prev, dif_neg hy, if_neg hz]
