---

Step * of Lemma equal-nil-lists

∀[T:Type]. ∀[x,y:Top List].  (x = y ∈ (T List)) supposing ((↑null(y)) and (↑null(x)))
BY
{ xxx(InductionOnList THEN InductionOnList THEN Reduce 0 THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x,y:Top  List].    (x  =  y)  supposing  ((\muparrow{}null(y))  and  (\muparrow{}null(x)))


By

---

Latex:
xxx(InductionOnList  THEN  InductionOnList  THEN  Reduce  0  THEN  Auto)xxx

---

Home Index