---

Step * of Lemma stable-union_wf

No Annotations
∀[X,T:Type]. ∀[P:T ⟶ X ⟶ ℙ].  (stable-union(X;T;i,x.P[i;x]) ∈ Type)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,T:Type].  \mforall{}[P:T  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}].    (stable-union(X;T;i,x.P[i;x])  \mmember{}  Type)


By

---

Latex:
ProveWfLemma

---

Home Index