---

Step * of Lemma omral_times_assoc_a

∀[g:OCMon]. ∀[a:CDRng]. ∀[ps,qs,rs:|omral(g;a)|].  ((ps ** (qs ** rs)) = ((ps ** qs) ** rs) ∈ |omral(g;a)|)
BY
{ (Auto
   THEN AssertLemma `omral_times_assoc` []
   THEN (Unfold `assoc` -1 THEN Unfold `infix_ap` -1 THEN RW (SweepUpC BetaC) (-1)⋅ THEN BHyp (-1) THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}[g:OCMon].  \mforall{}[a:CDRng].  \mforall{}[ps,qs,rs:|omral(g;a)|].    ((ps  **  (qs  **  rs))  =  ((ps  **  qs)  **  rs))


By

---

Latex:
(Auto
  THEN  AssertLemma  `omral\_times\_assoc`  []
  THEN  (Unfold  `assoc`  -1
              THEN  Unfold  `infix\_ap`  -1
              THEN  RW  (SweepUpC  BetaC)  (-1)\mcdot{}
              THEN  BHyp  (-1)
              THEN  Auto))

---

Home Index