---

Step * of Lemma W-induction1-extract

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[Q:W(A;a.B[a]) ⟶ ℙ].
  ((∀a:A. ∀f:B[a] ⟶ W(A;a.B[a]).  ((∀b:B[a]. Q[f b]) ⇒ Q[Wsup(a;f)])) ⇒ (∀w:W(A;a.B[a]). Q[w]))
BY
{ xxxExtract of Obid: W-induction1
     normalizes to:
     
     λF,w. (letrec H(par)=λw.let a,f = w in F a f (λb.(H Ax (f b))) in H(Ax) w)
     finishing with Autoxxx }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[Q:W(A;a.B[a])  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}a:A.  \mforall{}f:B[a]  {}\mrightarrow{}  W(A;a.B[a]).    ((\mforall{}b:B[a].  Q[f  b])  {}\mRightarrow{}  Q[Wsup(a;f)]))  {}\mRightarrow{}  (\mforall{}w:W(A;a.B[a]).  Q[w]))


By

---

Latex:
xxxExtract  of  Obid:  W-induction1
      normalizes  to:
     
      \mlambda{}F,w.  (letrec  H(par)=\mlambda{}w.let  a,f  =  w  in  F  a  f  (\mlambda{}b.(H  Ax  (f  b)))  in  H(Ax)  w)
      finishing  with  Autoxxx

---

Home Index