---

Step * of Lemma altWind_wf

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[P:altW(A;a.B[a]) ⟶ ℙ]. ∀[h:∀w:altW(A;a.B[a])
                                                         ((∀b:coW-dom(a.B[a];w). P[altW-item(w;b)]) ⇒ P[w])].
∀[w:altW(A;a.B[a])].
  (altWind(h;w) ∈ P[w])
BY
{ Auto }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. P : altW(A;a.B[a]) ⟶ ℙ
4. h : ∀w:altW(A;a.B[a]). ((∀b:coW-dom(a.B[a];w). P[altW-item(w;b)]) ⇒ P[w])
5. w : altW(A;a.B[a])
⊢ altWind(h;w) ∈ P[w]

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[P:altW(A;a.B[a])  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[h:\mforall{}w:altW(A;a.B[a])
                                                                                                                  ((\mforall{}b:coW-dom(a.B[a];w).  P[altW-item(w;b)])
                                                                                                                  {}\mRightarrow{}  P[w])].  \mforall{}[w:altW(A;a.B[a])].
    (altWind(h;w)  \mmember{}  P[w])


By

---

Latex:
Auto

---

Home Index