---

Step * 2 1 of Lemma W-type-induction


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

1
1. [A] : Type
2. eq : EqDecider(A)
3. ∀x,y:A.  Dec(x = y ∈ A)
4. [B] : A ⟶ Type
5. [P] : W-type(A; a.B[a]) ⟶ ℙ
6. ∀a:A. ∀f:B[a] ⟶ W-type(A; a.B[a]).  ((∀b:B[a]. P[f b]) ⇒ P[W-sup(a;f)])
7. a : A
8. w1 : B[a] ⟶ W-type(A; a.B[a])
9. ¬↑isr(Wselect(<a, w1>;[]))
10. ∀t:a:A ⟶ (B[a]?). case Wselect(<a, w1>;[t]) of inl(w) => P[w] | inr(z) => True
⊢ P[<a, w1>]

2
1. [A] : Type
2. eq : EqDecider(A)
3. ∀x,y:A.  Dec(x = y ∈ A)
4. [B] : A ⟶ Type
5. [P] : W-type(A; a.B[a]) ⟶ ℙ
6. ∀a:A. ∀f:B[a] ⟶ W-type(A; a.B[a]).  ((∀b:B[a]. P[f b]) ⇒ P[W-sup(a;f)])
7. u : a:A ⟶ (B[a]?)@i
8. v : (a:A ⟶ (B[a]?)) List@i
9. ∀w:W-type(A; a.B[a])
     ((¬↑isr(Wselect(w;v)))
     ⇒ (∀t:a:A ⟶ (B[a]?). case Wselect(w;v @ [t]) of inl(w) => P[w] | inr(z) => True)
     ⇒ case Wselect(w;v) of inl(w) => P[w] | inr(z) => True)
10. a : A
11. w1 : B[a] ⟶ W-type(A; a.B[a])
12. ¬↑isr(Wselect(<a, w1>;[u / v]))
13. ∀t:a:A ⟶ (B[a]?). case Wselect(<a, w1>;[u / (v @ [t])]) of inl(w) => P[w] | inr(z) => True
⊢ case Wselect(<a, w1>;[u / v]) of inl(w) => P[w] | inr(z) => True

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  eq  :  EqDecider(A)
3.  \mforall{}x,y:A.    Dec(x  =  y)
4.  [B]  :  A  {}\mrightarrow{}  Type
5.  [P]  :  W-type(A;  a.B[a])  {}\mrightarrow{}  \mBbbP{}
6.  \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)])
7.  w  :  W-type(A;  a.B[a])@i
8.  s  :  \{s:(a:A  {}\mrightarrow{}  (B[a]?))  List|  \mneg{}\muparrow{}isr(Wselect(w;s))\}  @i
9.  \mforall{}t:a:A  {}\mrightarrow{}  (B[a]?).  case  Wselect(w;s  @  [t])  of  inl(w)  =>  P[w]  |  inr(z)  =>  True
\mvdash{}  case  Wselect(w;s)  of  inl(w)  =>  P[w]  |  inr(z)  =>  True


By

---

Latex:
(MoveToConcl  (-1)\mcdot{}
  THEN  D  -1
  THEN  (Assert  \mneg{}\muparrow{}isr(Wselect(w;s))  BY
                          (Unhide  THEN  Auto))
  THEN  MoveToConcl  (-1)\mcdot{}
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-2)
  THEN  ListInd  (-1)
  THEN  TACTIC:(Reduce  0  THEN  Auto  THEN  WD  (-3)))\mcdot{}

---

Home Index