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