---

Step * of Lemma simple-comb0_wf

∀[Info,B:Type]. ∀[b:bag(B)].  (b| | ∈ EClass(B))
BY
{ (RepUR ``simple-comb0 simple-comb eclass`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[b:bag(B)].    (b|  |  \mmember{}  EClass(B))


By

---

Latex:
(RepUR  ``simple-comb0  simple-comb  eclass``  0  THEN  Auto)

---

Home Index