---

Step * 1 of Lemma W_iterate_functor_wf

.....assertion..... 
1. A : Type
2. B : A ⟶ Type
3. F : Type ⟶ Type
4. w : W(A;a.B[a])
⊢ ∀x:W(A;a.B[a]). ((x ≤  w) ⇒ (W_iterate_functor(A;a.B[a];T.F[T];x) ∈ Type))
BY
{ (WElim (-1) THEN RecUnfold `W_iterate_functor` 0 THEN Auto) }

1
1. A : Type
2. B : A ⟶ Type
3. F : Type ⟶ Type
4. a : A
5. f : B[a] ⟶ W(A;a.B[a])
6. ∀b:B[a]. ∀x:W(A;a.B[a]).  ((x ≤  (f b)) ⇒ (W_iterate_functor(A;a.B[a];T.F[T];x) ∈ Type))
7. x : W(A;a.B[a])
8. v : x ≤  Wsup(a;f)
9. ∀b:W(A;a.B[a]). (b <  x ∈ Type)
10. x1 : W(A;a.B[a])
11. x1 <  x
⊢ W_iterate_functor(A;a.B[a];T.F[T];x1) ∈ Type

---

Latex:

---

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


By

---

Latex:
(WElim  (-1)  THEN  RecUnfold  `W\_iterate\_functor`  0  THEN  Auto)

---

Home Index