---

Step * of Lemma cons-not-nil

∀[S:Type]. ∀[a:S]. ∀[b:S List].  (¬([a / b] = [] ∈ (S List)))
BY
{ (Auto THEN (D 0 THENA Auto)) }

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[a:S].  \mforall{}[b:S  List].    (\mneg{}([a  /  b]  =  []))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto))

---

Home Index