---

Step * 1 of Lemma altW-item_wf


1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. coW-wfdd(a.B[a];w)
5. b : coW-dom(a.B[a];w)
⊢ altW-item(w;b) ∈ coW(A;a.B[a])
BY
{ ProveWfLemma }

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  w  :  coW(A;a.B[a])
4.  coW-wfdd(a.B[a];w)
5.  b  :  coW-dom(a.B[a];w)
\mvdash{}  altW-item(w;b)  \mmember{}  coW(A;a.B[a])


By

---

Latex:
ProveWfLemma

---

Home Index