---

Step * of Lemma last_cons

∀[T:Type]. ∀[L:T List]. ∀[x:T].  last([x / L]) = last(L) ∈ T supposing ¬↑null(L)
BY
{ (((Auto THEN RWO "last_cons2" 0) THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[x:T].    last([x  /  L])  =  last(L)  supposing  \mneg{}\muparrow{}null(L)


By

---

Latex:
(((Auto  THEN  RWO  "last\_cons2"  0)  THENA  Auto)  THEN  AutoSplit)

---

Home Index