---

Step * of Lemma remove1_nil_lemma

∀a,s:Top.  ([] \ a ~ [])
BY
{ ((UnivCD THENA Auto) THEN RecUnfold `remove1` 0⋅ THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,s:Top.    ([]  \mbackslash{}  a  \msim{}  [])


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RecUnfold  `remove1`  0\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index