---

Step * of Lemma param-W-induction

∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type].
  ∀C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
    ∀[Q:par:P ⟶ (pW par) ⟶ ℙ]
      ((∀par:P. ∀a:A[par]. ∀f:b:B[par;a] ⟶ (pW C[par;a;b]).  ((∀b:B[par;a]. Q[C[par;a;b];f b]) ⇒ Q[par;pW-sup(a;f)]))
      ⇒ (∀par:P. ∀w:pW par.  Q[par;w]))
BY
{ ((UnivCD THENA Auto)
   THEN RenameVar `ind' 6
   THEN UseWitness ⌜let ind(p,a,f,G) = ind p a f G in 
                    letrec F(p,w) = let a,f=w in 
                                    ind(p,a,f,λb.F(C[p;a;b],f(b)) in 
                    F(par;w)⌝⋅
   THEN InstLemma `pW-rec_wf` [⌜P⌝;⌜A⌝;⌜B⌝;⌜C⌝;⌜Q⌝;⌜ind⌝;⌜par⌝;⌜w⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[A:P  {}\mrightarrow{}  Type].  \mforall{}[B:p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type].
    \mforall{}C:p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P
        \mforall{}[Q:par:P  {}\mrightarrow{}  (pW  par)  {}\mrightarrow{}  \mBbbP{}]
            ((\mforall{}par:P.  \mforall{}a:A[par].  \mforall{}f:b:B[par;a]  {}\mrightarrow{}  (pW  C[par;a;b]).
                    ((\mforall{}b:B[par;a].  Q[C[par;a;b];f  b])  {}\mRightarrow{}  Q[par;pW-sup(a;f)]))
            {}\mRightarrow{}  (\mforall{}par:P.  \mforall{}w:pW  par.    Q[par;w]))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RenameVar  `ind'  6
  THEN  UseWitness  \mkleeneopen{}let  ind(p,a,f,G)  =  ind  p  a  f  G  in 
                                    letrec  F(p,w)  =  let  a,f=w  in 
                                                                    ind(p,a,f,\mlambda{}b.F(C[p;a;b],f(b))  in 
                                    F(par;w)\mkleeneclose{}\mcdot{}
  THEN  InstLemma  `pW-rec\_wf`  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}Q\mkleeneclose{};\mkleeneopen{}ind\mkleeneclose{};\mkleeneopen{}par\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index