---

Step * 1 1 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
7. [u / v] ~ []
8. 1 ~ 0
⊢ False
BY
{ ((Assert 0 = 1 ∈ ℤ BY (RWO  "-1" 0 THEN Auto)) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  0  =  1  BY  (RWO    "-1"  0  THEN  Auto))  THEN  Auto)

---

Home Index