---

Step * of Lemma add-commutes

∀[x:ℤ]. ∀[y:Top].  (x + y ~ y + x)
BY
{ TACTIC:Assert ⌜∀x,y:ℤ.  ((x + y) = (y + x) ∈ ℤ)⌝⋅ }

1
.....assertion..... 
∀x,y:ℤ.  ((x + y) = (y + x) ∈ ℤ)

2
1. ∀x,y:ℤ.  ((x + y) = (y + x) ∈ ℤ)
⊢ ∀[x:ℤ]. ∀[y:Top].  (x + y ~ y + x)

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  \mforall{}[y:Top].    (x  +  y  \msim{}  y  +  x)


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mforall{}x,y:\mBbbZ{}.    ((x  +  y)  =  (y  +  x))\mkleeneclose{}\mcdot{}

---

Home Index