---

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


1. 0 = 1 ∈ ℤ
2. 0 ~ 1
3. if 0=1 then False else True
⊢ False
BY
{ Refine_sqequalHypSubstitution 3 ⌜0 ~ 1⌝ `z' ⌜if z=1 then False else True⌝⋅ }

1
1. 0 = 1 ∈ ℤ
2. 0 ~ 1
3. if 0=1 then False else True
⊢ 0 ~ 1

2
1. 0 = 1 ∈ ℤ
2. 0 ~ 1
3. if 1=1 then False else True
⊢ False

---

Latex:

---

Latex:

1.  0  =  1
2.  0  \msim{}  1
3.  if  0=1  then  False  else  True
\mvdash{}  False


By

---

Latex:
Refine\_sqequalHypSubstitution  3  \mkleeneopen{}0  \msim{}  1\mkleeneclose{}  `z'  \mkleeneopen{}if  z=1  then  False  else  True\mkleeneclose{}\mcdot{}

---

Home Index