---

Step * 2 of Lemma W_iterate_functor_wf


1. A : Type
2. B : A ⟶ Type
3. F : Type ⟶ Type
4. w : W(A;a.B[a])
5. ∀x:W(A;a.B[a]). ((x ≤  w) ⇒ (W_iterate_functor(A;a.B[a];T.F[T];x) ∈ Type))
⊢ W_iterate_functor(A;a.B[a];T.F[T];w) ∈ Type
BY
{ (InstHyp [⌜w⌝] (-1)⋅ THEN EAuto 1) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  F  :  Type  {}\mrightarrow{}  Type
4.  w  :  W(A;a.B[a])
5.  \mforall{}x:W(A;a.B[a]).  ((x  \mleq{}    w)  {}\mRightarrow{}  (W\_iterate\_functor(A;a.B[a];T.F[T];x)  \mmember{}  Type))
\mvdash{}  W\_iterate\_functor(A;a.B[a];T.F[T];w)  \mmember{}  Type


By

---

Latex:
(InstHyp  [\mkleeneopen{}w\mkleeneclose{}]  (-1)\mcdot{}  THEN  EAuto  1)

---

Home Index