---

Step * 1 of Lemma not-0-eq-1


1. 0 = 1 ∈ ℤ
⊢ False
BY
{ (Assert 0 ~ 1 BY
         (Refine_sqequalBase THEN Refine_baseInt THEN Hypothesis)) }

1
1. 0 = 1 ∈ ℤ
2. 0 ~ 1
⊢ False

---

Latex:

---

Latex:

1.  0  =  1
\mvdash{}  False


By

---

Latex:
(Assert  0  \msim{}  1  BY
              (Refine\_sqequalBase  THEN  Refine\_baseInt  THEN  Hypothesis))

---

Home Index