---

Step * 1 1 1 of Lemma W-sup_wf


1. A : Type
2. B : A ⟶ Type
3. a : A
4. f : B[a] ⟶ W-type(A; a.B[a])
5. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
6. W-sup(a;f) ∈ co-W(A;a.B[a])
7. ↑isl(p 0 a)
8. n : ℕ
9. n + 1 ≠ 0
10. ↑isr(W-select(f outl(p 0 a);map(λn.(p (n + 1));upto(n))))
⊢ ↑isr(case p 0 a of inl(b) => W-select(f b;map(p;map(λi.(i + 1);upto((n + 1) - 1)))) | inr(z) => inr z )
BY
{ (MoveToConcl (-1) THEN MoveToConcl (-3) THEN (GenConclTerm ⌜p 0 a⌝⋅ THENA Auto) THEN D (-2) THEN Reduce 0 THEN Auto)
⋅ }

1
1. A : Type
2. B : A ⟶ Type
3. a : A
4. f : B[a] ⟶ W-type(A; a.B[a])
5. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
6. W-sup(a;f) ∈ co-W(A;a.B[a])
7. n : ℕ
8. n + 1 ≠ 0
9. x : B[a]@i
10. (p 0 a) = (inl x) ∈ (B[a]?)
11. True
12. ↑isr(W-select(f x;map(λn.(p (n + 1));upto(n))))
⊢ ↑isr(W-select(f x;map(p;map(λi.(i + 1);upto((n + 1) - 1)))))

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  a  :  A
4.  f  :  B[a]  {}\mrightarrow{}  W-type(A;  a.B[a])
5.  p  :  \mBbbN{}  {}\mrightarrow{}  a:A  {}\mrightarrow{}  (B[a]?)@i
6.  W-sup(a;f)  \mmember{}  co-W(A;a.B[a])
7.  \muparrow{}isl(p  0  a)
8.  n  :  \mBbbN{}
9.  n  +  1  \mneq{}  0
10.  \muparrow{}isr(W-select(f  outl(p  0  a);map(\mlambda{}n.(p  (n  +  1));upto(n))))
\mvdash{}  \muparrow{}isr(case  p  0  a
  of  inl(b)  =>
  W-select(f  b;map(p;map(\mlambda{}i.(i  +  1);upto((n  +  1)  -  1))))
  |  inr(z)  =>
  inr  z  )


By

---

Latex:
(MoveToConcl  (-1)
  THEN  MoveToConcl  (-3)
  THEN  (GenConclTerm  \mkleeneopen{}p  0  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  (-2)
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index