---

Step * 1 of Lemma W-type-induction


1. [A] : Type
2. ∀x,y:A.  Dec(x = y ∈ A)
3. [B] : A ⟶ Type
4. [P] : W-type(A; a.B[a]) ⟶ ℙ
5. ∀a:A. ∀f:B[a] ⟶ W-type(A; a.B[a]).  ((∀b:B[a]. P[f b]) ⇒ P[W-sup(a;f)])
6. w : W-type(A; a.B[a])@i
7. s : {s:(a:A ⟶ (B[a]?)) List| ↑isr(Wselect(w;s))} @i
⊢ case Wselect(w;s) of inl(w) => P[w] | inr(z) => True
BY
{ ((Assert ↑isr(Wselect(w;s)) BY
          (D (-1)⋅ THEN Unhide THEN Auto))
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜Wselect(w;s)⌝⋅ THENA Auto)
   THEN D (-2) 
   THEN Reduce 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  \mforall{}x,y:A.    Dec(x  =  y)
3.  [B]  :  A  {}\mrightarrow{}  Type
4.  [P]  :  W-type(A;  a.B[a])  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}a:A.  \mforall{}f:B[a]  {}\mrightarrow{}  W-type(A;  a.B[a]).    ((\mforall{}b:B[a].  P[f  b])  {}\mRightarrow{}  P[W-sup(a;f)])
6.  w  :  W-type(A;  a.B[a])@i
7.  s  :  \{s:(a:A  {}\mrightarrow{}  (B[a]?))  List|  \muparrow{}isr(Wselect(w;s))\}  @i
\mvdash{}  case  Wselect(w;s)  of  inl(w)  =>  P[w]  |  inr(z)  =>  True


By

---

Latex:
((Assert  \muparrow{}isr(Wselect(w;s))  BY
                (D  (-1)\mcdot{}  THEN  Unhide  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}Wselect(w;s)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  (-2) 
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index