---

Step * of Lemma before_last_or

∀[T:Type]. ∀L:T List. ∀x:T.  ((x ∈ L) ⇒ ((x = last(L) ∈ T) ∨ x before last(L) ∈ L))
BY
{ (Auto THEN RepeatFor 2 (D (-1)) THEN (Decide ⌜i = (||L|| - 1) ∈ ℤ⌝⋅ THENA Auto)) }

1
1. [T] : Type
2. L : T List
3. x : T
4. i : ℕ
5. i < ||L||
6. x = L[i] ∈ T
7. i = (||L|| - 1) ∈ ℤ
⊢ (x = last(L) ∈ T) ∨ x before last(L) ∈ L

2
1. [T] : Type
2. L : T List
3. x : T
4. i : ℕ
5. i < ||L||
6. x = L[i] ∈ T
7. ¬(i = (||L|| - 1) ∈ ℤ)
⊢ (x = last(L) ∈ T) ∨ x before last(L) ∈ L

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}x:T.    ((x  \mmember{}  L)  {}\mRightarrow{}  ((x  =  last(L))  \mvee{}  x  before  last(L)  \mmember{}  L))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (D  (-1))  THEN  (Decide  \mkleeneopen{}i  =  (||L||  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index