---

Step * 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)
⊢ W-bars(W-sup(a;f);p)
BY
{ (Assert W-bars(f outl(p 0 a);λn.(p (n + 1))) BY
         ((GenConclTerm ⌜f outl(p 0 a)⌝⋅ THENA Auto)
          THEN Try ((D (-2) THEN Unhide THEN Auto))
          THEN MoveToConcl (-1)
          THEN GenConclTerm ⌜p 0⌝⋅
          THEN Auto
          THEN DVar `v'
          THEN All Reduce
          THEN RW assert_pushdownC (-1)
          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. ↑isl(p 0 a)
8. W-bars(f outl(p 0 a);λn.(p (n + 1)))
⊢ W-bars(W-sup(a;f);p)

---

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)
\mvdash{}  W-bars(W-sup(a;f);p)


By

---

Latex:
(Assert  W-bars(f  outl(p  0  a);\mlambda{}n.(p  (n  +  1)))  BY
              ((GenConclTerm  \mkleeneopen{}f  outl(p  0  a)\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  Try  ((D  (-2)  THEN  Unhide  THEN  Auto))
                THEN  MoveToConcl  (-1)
                THEN  GenConclTerm  \mkleeneopen{}p  0\mkleeneclose{}\mcdot{}
                THEN  Auto
                THEN  DVar  `v'
                THEN  All  Reduce
                THEN  RW  assert\_pushdownC  (-1)
                THEN  Auto))\mcdot{}

---

Home Index