---

Step * 2 1 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. 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>]
BY
{ (Fold `W-sup` 0
   THEN BackThruSomeHyp
   THEN TACTIC:Auto
   THEN (InstHyp [⌜λz.if eq z a then inl b else inr ⋅  fi ⌝] (-2)⋅ THENA Auto)
   THEN Unfold `Wselect` -1
   THEN RecUnfold `W-select` (-1)⋅
   THEN Fold `Wselect` (-1)
   THEN Reduce (-1)
   THEN SplitOnHypITE -1 ⋅
   THEN Auto)⋅ }

---

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.  a  :  A
8.  w1  :  B[a]  {}\mrightarrow{}  W-type(A;  a.B[a])
9.  \mneg{}\muparrow{}isr(Wselect(<a,  w1>[]))
10.  \mforall{}t:a:A  {}\mrightarrow{}  (B[a]?).  case  Wselect(<a,  w1>[t])  of  inl(w)  =>  P[w]  |  inr(z)  =>  True
\mvdash{}  P[<a,  w1>]


By

---

Latex:
(Fold  `W-sup`  0
  THEN  BackThruSomeHyp
  THEN  TACTIC:Auto
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}z.if  eq  z  a  then  inl  b  else  inr  \mcdot{}    fi  \mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  Unfold  `Wselect`  -1
  THEN  RecUnfold  `W-select`  (-1)\mcdot{}
  THEN  Fold  `Wselect`  (-1)
  THEN  Reduce  (-1)
  THEN  SplitOnHypITE  -1  \mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index