---

Step * 1 4 of Lemma oal_grp_wf


1. s : LOSet@i'
2. g : AbDGrp@i'
⊢ Comm(|oal(s;g)|;λx,y. (x ++ y))
BY
{ ((Force `5` (Eval ``comm`` 0) 
THENM Backchain ``oal_merge_comm``) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  AbDGrp@i'
\mvdash{}  Comm(|oal(s;g)|;\mlambda{}x,y.  (x  ++  y))


By

---

Latex:
((Force  `5`  (Eval  ``comm``  0) 
THENM  Backchain  ``oal\_merge\_comm``)  THEN  Auto)

---

Home Index