---

Step * of Lemma RankEx2_UnionList-unionlist_wf

∀[S,T:Type]. ∀[v:RankEx2(S;T)].
  RankEx2_UnionList-unionlist(v) ∈ T + (RankEx2(S;T) List) supposing ↑RankEx2_UnionList?(v)
BY
{ DepprodCoDatatypeSelectorWf }

---

Latex:

---

Latex:
\mforall{}[S,T:Type].  \mforall{}[v:RankEx2(S;T)].
    RankEx2\_UnionList-unionlist(v)  \mmember{}  T  +  (RankEx2(S;T)  List)  supposing  \muparrow{}RankEx2\_UnionList?(v)


By

---

Latex:
DepprodCoDatatypeSelectorWf

---

Home Index