---

Step * of Lemma nil-not-cons

∀[S:Type]. ∀[a:S]. ∀[b:S List].  (¬([] = [a / b] ∈ (S List)))
BY
{ (InstLemma `cons-not-nil` [] THEN RepeatFor 4 (ParallelLast')) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `cons-not-nil`  []  THEN  RepeatFor  4  (ParallelLast'))

---

Home Index