---

Step * of Lemma not-cons-sq-nil

∀[u,v:Top].  (([u / v] ~ []) = (0 ~ 1) ∈ Type)
BY
{ (Auto
   THEN (PointwiseFunctionalityForEquality 1 THENW Auto)
   THEN (PointwiseFunctionalityForEquality (-1) THENW Auto)) }

1
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

---

Latex:

---

Latex:
\mforall{}[u,v:Top].    (([u  /  v]  \msim{}  [])  =  (0  \msim{}  1))


By

---

Latex:
(Auto
  THEN  (PointwiseFunctionalityForEquality  1  THENW  Auto)
  THEN  (PointwiseFunctionalityForEquality  (-1)  THENW  Auto))

---

Home Index