---

Step * 1 of Lemma not-cons-sq-nil


1. u : Base
2. u1 : Base
3. u = u1 ∈ Top
4. v : Base
5. v1 : Base
6. v = v1 ∈ Top
⊢ ([u / v] ~ []) = (0 ~ 1) ∈ Type
BY
{ ((BLemma `false-sqequal` THEN Auto) THEN (D 0 THENA Auto)) }

1
1. u : Base
2. u1 : Base
3. u = u1 ∈ Top
4. v : Base
5. v1 : Base
6. v = v1 ∈ Top
7. [u / v] ~ []
⊢ False

---

Latex:

---

Latex:

1.  u  :  Base
2.  u1  :  Base
3.  u  =  u1
4.  v  :  Base
5.  v1  :  Base
6.  v  =  v1
\mvdash{}  ([u  /  v]  \msim{}  [])  =  (0  \msim{}  1)


By

---

Latex:
((BLemma  `false-sqequal`  THEN  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index