---

Step * of Lemma cons_functionality_wrt_permr_massoc

∀g:IAbMonoid. ∀a,b:|g|. ∀as,bs:|g| List.  ((a ~ b) ⇒ as ≡ bs upto ~ ⇒ [a / as] ≡ [b / bs] upto ~)
BY
{ Unfold `permr_massoc` 0 
THEN Backchain ``cons_functionality_wrt_permr_upto 
  massoc_equiv_rel`` 
THEN Auto }

---

Latex:

---

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


By

---

Latex:
Unfold  `permr\_massoc`  0 
THEN  Backchain  ``cons\_functionality\_wrt\_permr\_upto 
    massoc\_equiv\_rel`` 
THEN  Auto

---

Home Index