---

Step * of Lemma prior-as-rec-bind-class-in_wf

∀[Info,A:Type]. ∀[X:EClass(A)]. ∀[i:Top + bag(A) + Top].  (prior-as-rec-bind-class-in(X;i) ∈ EClass(bag(A) + (bag(A)?)))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[i:Top  +  bag(A)  +  Top].
    (prior-as-rec-bind-class-in(X;i)  \mmember{}  EClass(bag(A)  +  (bag(A)?)))


By

---

Latex:
ProveWfLemma

---

Home Index