---

Step * of Lemma not_permr_cons_nil

∀T:Type. ∀a:T. ∀as:T List.  (¬([a / as] ≡(T) []))
BY
{ ((UnivCD THENM D 0) THENA Auto) }

1
1. T : Type
2. a : T
3. as : T List
4. [a / as] ≡(T) []
⊢ False

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}a:T.  \mforall{}as:T  List.    (\mneg{}([a  /  as]  \mequiv{}(T)  []))


By

---

Latex:
((UnivCD  THENM  D  0)  THENA  Auto)

---

Home Index