---

Step * of Lemma void-list-equality3

∀[x,y:Void List].  {(↑null(x)) ∧ (↑null(y))} supposing x = y ∈ (Void List)
BY
{ xxx(InductionOnList THEN InductionOnList THEN Reduce 0 THEN Auto THEN Unfold `guard` 0 THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[x,y:Void  List].    \{(\muparrow{}null(x))  \mwedge{}  (\muparrow{}null(y))\}  supposing  x  =  y


By

---

Latex:
xxx(InductionOnList  THEN  InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  Unfold  `guard`  0  THEN  Auto)xxx

---

Home Index