---

Step * of Lemma permr_massoc_weakening

∀g:IAbMonoid. ∀as,bs:|g| List.  ((as ≡(|g|) bs) ⇒ as ≡ bs upto ~)
BY
{ Unfold `permr_massoc` 0 
THEN Backchain ``permr_upto_weakening 
  massoc_equiv_rel`` 
THEN Auto }

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  \mforall{}as,bs:|g|  List.    ((as  \mequiv{}(|g|)  bs)  {}\mRightarrow{}  as  \mequiv{}  bs  upto  \msim{})


By

---

Latex:
Unfold  `permr\_massoc`  0 
THEN  Backchain  ``permr\_upto\_weakening 
    massoc\_equiv\_rel`` 
THEN  Auto

---

Home Index