---

Step * 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] ~ []
⊢ False
BY
{ ((Assert if [u / v] = Ax then 0 otherwise 1 ~ if [] = Ax then 0 otherwise 1 BY Auto) THEN Reduce -1) }

1
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

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  if  [u  /  v]  =  Ax  then  0  otherwise  1  \msim{}  if  []  =  Ax  then  0  otherwise  1  BY  Auto)  THEN  Reduce  -1)

---

Home Index