---

Step * 2 of Lemma nil-contains


1. [T] : Type
2. u : T
3. v : T List
⊢ [u / v] ⊆ [] ⇐⇒ False
BY
{ (Auto THEN With ⌜0⌝ (D (-1))⋅ THEN Reduce 0 THEN Auto') }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  u  :  T
3.  v  :  T  List
\mvdash{}  [u  /  v]  \msubseteq{}  []  \mLeftarrow{}{}\mRightarrow{}  False


By

---

Latex:
(Auto  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  (-1))\mcdot{}  THEN  Reduce  0  THEN  Auto')

---

Home Index