---

Step * of Lemma mul-swap

∀[x:ℤ]. ∀[y,z:Top].  (x * y * z ~ y * x * z)
BY
{ ((UnivCD THENA Auto)
   THEN (RW (AddrC [1] (RevLemmaC `mul-associates`)) 0 THENA Trivial)
   THEN (RW (AddrC [1;1] (LemmaC `mul-commutes`)) 0 THENA Trivial)
   THEN (RW (AddrC [1] (LemmaC `mul-associates`)) 0 THENA Trivial)) }

1
1. x : ℤ
2. y : Top
3. z : Top
⊢ y * x * z ~ y * x * z

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RW  (AddrC  [1]  (RevLemmaC  `mul-associates`))  0  THENA  Trivial)
  THEN  (RW  (AddrC  [1;1]  (LemmaC  `mul-commutes`))  0  THENA  Trivial)
  THEN  (RW  (AddrC  [1]  (LemmaC  `mul-associates`))  0  THENA  Trivial))

---

Home Index