---

Step * 1 1 2 of Lemma W_iterate_functor_wf


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
12. x1 <  Wsup(a;f)
⊢ W_iterate_functor(A;a.B[a];T.F[T];x1) ∈ Type
BY
{ (RecUnfold `Wcmp` (-1)
   THEN Reduce (-1)
   THEN D -1
   THEN RenameVar `b' (-2)
   THEN (InstHyp[⌜b⌝] 6⋅ THENA Auto)
   THEN BHyp -1 
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  F  :  Type  {}\mrightarrow{}  Type
4.  a  :  A
5.  f  :  B[a]  {}\mrightarrow{}  W(A;a.B[a])
6.  \mforall{}b:B[a].  \mforall{}x:W(A;a.B[a]).    ((x  \mleq{}    (f  b))  {}\mRightarrow{}  (W\_iterate\_functor(A;a.B[a];T.F[T];x)  \mmember{}  Type))
7.  x  :  W(A;a.B[a])
8.  v  :  x  \mleq{}    Wsup(a;f)
9.  \mforall{}b:W(A;a.B[a]).  (b  <    x  \mmember{}  Type)
10.  x1  :  W(A;a.B[a])
11.  x1  <    x
12.  x1  <    Wsup(a;f)
\mvdash{}  W\_iterate\_functor(A;a.B[a];T.F[T];x1)  \mmember{}  Type


By

---

Latex:
(RecUnfold  `Wcmp`  (-1)
  THEN  Reduce  (-1)
  THEN  D  -1
  THEN  RenameVar  `b'  (-2)
  THEN  (InstHyp[\mkleeneopen{}b\mkleeneclose{}]  6\mcdot{}  THENA  Auto)
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index