---

Step * of Lemma append_is_nil

∀[T:Type]. ∀[l1,l2:T List].  uiff((l1 @ l2) = [] ∈ (T List);(l1 = [] ∈ (T List)) ∧ (l2 = [] ∈ (T List)))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l1,l2:T  List].    uiff((l1  @  l2)  =  [];(l1  =  [])  \mwedge{}  (l2  =  []))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index