---

Step * 1 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)
⊢ W-bars(x1 b;p)
BY
{ ((InstHyp [⌜λn.if (n =z 0) then λz.if eq z a then inl b else inr ⋅  fi  else p (n - 1) fi ⌝] (-4)⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN ExRepD
   THEN TACTIC:CaseNat 0 `n')⋅ }

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 ∈ ℤ
⊢ ∃n:ℕ. (↑isr(W-select(x1 b;map(p;upto(n)))))

2
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)))))

---

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)
\mvdash{}  W-bars(x1  b;p)


By

---

Latex:
((InstHyp  [\mkleeneopen{}\mlambda{}n.if  (n  =\msubz{}  0)  then  \mlambda{}z.if  eq  z  a  then  inl  b  else  inr  \mcdot{}    fi    else  p  (n  -  1)  fi  \mkleeneclose{}]  (-4)\mcdot{}
    THENA  Auto
    )
  THEN  RepeatFor  2  (ParallelLast)
  THEN  ExRepD
  THEN  TACTIC:CaseNat  0  `n')\mcdot{}

---

Home Index