---

Step * of Lemma W_ind_wf

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[Q:W(A;a.B[a]) ⟶ ℙ].
∀[F:∀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])].
  (W_ind(F;w) ∈ Q[w])
BY
{ ((Assert ⌜TERMOF{W-induction1-extract:o, \\v:l, i:l} ∈ ∀[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]))⌝⋅
    THENA Auto
    )
   THEN Auto
   THEN (Assert TERMOF{W-induction1-extract:o, \\v:l, i:l} ∈ (∀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
               Auto)
   THEN Thin 1
   THEN (Assert TERMOF{W-induction1-extract:o, \\v:l, i:l} F w ∈ Q[w] BY
               Auto)
   THEN Thin (-2)
   THEN NthHypSq (-1)
   THEN EqCD
   THEN Auto
   THEN RW (SubC (SymbCompC [] 100)) 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[Q:W(A;a.B[a])  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[F:\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)])].
\mforall{}[w:W(A;a.B[a])].
    (W\_ind(F;w)  \mmember{}  Q[w])


By

---

Latex:
((Assert  \mkleeneopen{}TERMOF\{W-induction1-extract:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}
                    \mmember{}  \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]))\mkleeneclose{}\mcdot{}
    THENA  Auto
    )
  THEN  Auto
  THEN  (Assert  TERMOF\{W-induction1-extract:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  \mmember{}  (\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
                          Auto)
  THEN  Thin  1
  THEN  (Assert  TERMOF\{W-induction1-extract:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  F  w  \mmember{}  Q[w]  BY
                          Auto)
  THEN  Thin  (-2)
  THEN  NthHypSq  (-1)
  THEN  EqCD
  THEN  Auto
  THEN  RW  (SubC  (SymbCompC  []  100))  0
  THEN  Auto)

---

Home Index