---

Step * of Lemma W-induction1

∀[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
{ ((UnivCD THENA Auto)
   THEN (InstLemma `param-W-induction` [⌜Unit⌝;⌜λ2p.A⌝;⌜λ2p a.B[a]⌝;⌜so_lambda(p,a,b.⋅)⌝;⌜λ2p w.Q[w]⌝]⋅ THENA Auto)
   THEN Try (DProds)
   THEN All (Fold `it`)
   THEN All (Fold `W`)
   THEN Try (Trivial)) }

1
1. [A] : Type
2. [B] : A ⟶ Type
3. [Q] : W(A;a.B[a]) ⟶ ℙ
4. ∀a:A. ∀f:B[a] ⟶ W(A;a.B[a]).  ((∀b:B[a]. Q[f b]) ⇒ Q[Wsup(a;f)])@i
5. w : W(A;a.B[a])@i
6. par : 0 = 0 ∈ ℤ
7. a : A@i
8. f : b:B[a] ⟶ W(A;a.B[a])@i
9. ∀b:B[a]. Q[f b]@i
⊢ Q[pW-sup(a;f)]

2
1. [A] : Type
2. [B] : A ⟶ Type
3. [Q] : W(A;a.B[a]) ⟶ ℙ
4. ∀a:A. ∀f:B[a] ⟶ W(A;a.B[a]).  ((∀b:B[a]. Q[f b]) ⇒ Q[Wsup(a;f)])@i
5. w : W(A;a.B[a])@i
6. ∀par:Unit. ∀w:pW par.  Q[w]
⊢ Q[w]

---

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:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `param-W-induction`  [\mkleeneopen{}Unit\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p  a.B[a]\mkleeneclose{};\mkleeneopen{}so\_lambda(p,a,b.\mcdot{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p  w.Q[w]\mkleeneclose{}]
              \mcdot{}
              THENA  Auto
              )
  THEN  Try  (DProds)
  THEN  All  (Fold  `it`)
  THEN  All  (Fold  `W`)
  THEN  Try  (Trivial))

---

Home Index