---

Step * 1 2 of Lemma W-type-ext


1. A : Type
2. ∀x,y:A.  Dec(x = y ∈ A)
3. B : A ⟶ Type
4. a : A
5. x1 : B[a] ⟶ co-W(A;a.B[a])
6. ∀p:ℕ ⟶ a:A ⟶ (B[a]?). W-bars(<a, x1>;p)
7. b : B[a]
8. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
9. eq : EqDecider(A)
10. n : ℕ
11. ↑isr(W-select(<a, x1>;map(λn.if (n =z 0) then λz.if eq z a then inl b else inr ⋅  fi  else p (n - 1) fi ;upto(n))))
12. ¬(n = 0 ∈ ℤ)
⊢ ∃n:ℕ. (↑isr(W-select(x1 b;map(p;upto(n)))))
BY
{ (With ⌜n - 1⌝ (D 0)⋅ THEN Auto)⋅ }

1
1. A : Type
2. ∀x,y:A.  Dec(x = y ∈ A)
3. B : A ⟶ Type
4. a : A
5. x1 : B[a] ⟶ co-W(A;a.B[a])
6. ∀p:ℕ ⟶ a:A ⟶ (B[a]?). W-bars(<a, x1>;p)
7. b : B[a]
8. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
9. eq : EqDecider(A)
10. n : ℕ
11. ↑isr(W-select(<a, x1>;map(λn.if (n =z 0) then λz.if eq z a then inl b else inr ⋅  fi  else p (n - 1) fi ;upto(n))))
12. ¬(n = 0 ∈ ℤ)
⊢ ↑isr(W-select(x1 b;map(p;upto(n - 1))))

---

Latex:

---

Latex:

1.  A  :  Type
2.  \mforall{}x,y:A.    Dec(x  =  y)
3.  B  :  A  {}\mrightarrow{}  Type
4.  a  :  A
5.  x1  :  B[a]  {}\mrightarrow{}  co-W(A;a.B[a])
6.  \mforall{}p:\mBbbN{}  {}\mrightarrow{}  a:A  {}\mrightarrow{}  (B[a]?).  W-bars(<a,  x1>p)
7.  b  :  B[a]
8.  p  :  \mBbbN{}  {}\mrightarrow{}  a:A  {}\mrightarrow{}  (B[a]?)@i
9.  eq  :  EqDecider(A)
10.  n  :  \mBbbN{}
11.  \muparrow{}isr(W-select(<a,  x1>map(\mlambda{}n.if  (n  =\msubz{}  0)  then  \mlambda{}z.if  eq  z  a  then  inl  b  else  inr  \mcdot{}    fi    else  p  (n  \000C-  1)  fi  ;
                        upto(n))))
12.  \mneg{}(n  =  0)
\mvdash{}  \mexists{}n:\mBbbN{}.  (\muparrow{}isr(W-select(x1  b;map(p;upto(n)))))


By

---

Latex:
(With  \mkleeneopen{}n  -  1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index