Step * of Lemma mul-swap

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

1
1. : ℤ
2. Top
3. Top
⊢ 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