---

Step * 1 of Lemma respects-equality-oalist1


1. s : LOSet
2. g : AbDMon
⊢ respects-equality(|(s × (g↓set))| List;|oal(s;g)|)
BY
{ (RepUR ``set_car oalist dset_set mk_dset dset_of_mon set_prod`` 0 THEN D -1 THEN D -2 THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  LOSet
2.  g  :  AbDMon
\mvdash{}  respects-equality(|(s  \mtimes{}  (g\mdownarrow{}set))|  List;|oal(s;g)|)


By

---

Latex:
(RepUR  ``set\_car  oalist  dset\_set  mk\_dset  dset\_of\_mon  set\_prod``  0  THEN  D  -1  THEN  D  -2  THEN  Auto)

---

Home Index