---

Step * of Lemma listp_decomp

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

---

Latex:

---

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


By

---

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

---

Home Index