---

Step * of Lemma cons_neq_nil

∀[T:Type]. ∀[h:T]. ∀[t:T List].  (¬([h / t] = [] ∈ (T List)))
BY
{ ((Unfold `not` 0 THEN UnivCD) THENA Auto) }

1
1. T : Type
2. h : T
3. t : T List
4. [h / t] = [] ∈ (T List)
⊢ False

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[h:T].  \mforall{}[t:T  List].    (\mneg{}([h  /  t]  =  []))


By

---

Latex:
((Unfold  `not`  0  THEN  UnivCD)  THENA  Auto)

---

Home Index