---

Step * of Lemma false-sqequal

∀[a,b:Base].  ((¬(a ~ b)) ⇒ ((a ~ b) = (0 ~ 1) ∈ Type))
BY
{ (Auto THEN Refine_sqequalExtensionalEquality THEN D 0 THEN Auto) }

1
1. a : Base
2. b : Base
3. ¬(a ~ b)
4. 0 ~ 1
⊢ a = b ∈ Base

---

Latex:

---

Latex:
\mforall{}[a,b:Base].    ((\mneg{}(a  \msim{}  b))  {}\mRightarrow{}  ((a  \msim{}  b)  =  (0  \msim{}  1)))


By

---

Latex:
(Auto  THEN  Refine\_sqequalExtensionalEquality  THEN  D  0  THEN  Auto)

---

Home Index