---

Step * 1 of Lemma before_last


1. [T] : Type
⊢ ∀x:T. ((x ∈ []) ⇒ x before last([]) ∈ [] supposing ¬(x = last([]) ∈ T))
BY
{ (((D 0 THENM D 0) THENM RWO "nil_member" (-1)) THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  \mforall{}x:T.  ((x  \mmember{}  [])  {}\mRightarrow{}  x  before  last([])  \mmember{}  []  supposing  \mneg{}(x  =  last([])))


By

---

Latex:
(((D  0  THENM  D  0)  THENM  RWO  "nil\_member"  (-1))  THEN  Auto)

---

Home Index