---

Step * of Lemma listp_decomp_last

∀[T:Type]. ∀L:T List+. ∃K:T List. (L = (K @ [last(L)]) ∈ (T List))
BY
{ (Auto THEN D (-1) THEN BLemma `list_decomp_last` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List\msupplus{}.  \mexists{}K:T  List.  (L  =  (K  @  [last(L)]))


By

---

Latex:
(Auto  THEN  D  (-1)  THEN  BLemma  `list\_decomp\_last`  THEN  Auto)

---

Home Index