---

Step * of Lemma oalist_wf

∀a:LOSet. ∀b:AbDMon.  (oal(a;b) ∈ DSet)
BY
{ (Auto THEN (Assert b ∈ GrpSig BY (RepeatFor 2 (DVar `b') THEN Auto)) THEN Unfold `oalist` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.    (oal(a;b)  \mmember{}  DSet)


By

---

Latex:
(Auto
  THEN  (Assert  b  \mmember{}  GrpSig  BY
                          (RepeatFor  2  (DVar  `b')  THEN  Auto))
  THEN  Unfold  `oalist`  0  THEN  Auto)

---

Home Index