---

Step * 1 1 of Lemma two-mul

.....equality..... 
1. x : ℤ
⊢ 2 ~ 1 + 1
BY
{ (Reduce 0 THEN SqReflexive) }

---

Latex:

---

Latex:
.....equality..... 
1.  x  :  \mBbbZ{}
\mvdash{}  2  \msim{}  1  +  1


By

---

Latex:
(Reduce  0  THEN  SqReflexive)

---

Home Index