---

Step * 1 of Lemma pW-sup_wf


1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pco-W ∈ P ⟶ Type
6. par : P
7. a : A[par]
8. f : b:B[par;a] ⟶ (pW C[par;a;b])
⊢ pW-sup(a;f) ∈ pW par
BY
{ TACTIC:((Assert pW-sup(a;f) ∈ pco-W par BY
                 (pcoWD 0
                  THEN Auto
                  THEN ProveWfLemma
                  THEN (ExtWith [`b'] [b:B[par;a] ⟶ (pW C[par;a;b])]⋅
                        THEN Auto
                        THEN DoSubsume
                        THEN Auto
                        THEN (Unfold `param-W` 0 THEN Reduce 0)
                        THEN Auto)⋅))
          THEN (Unfold `param-W` 0 THEN Reduce 0 THEN MemTypeCD THEN Auto)⋅
          ) }

1
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pco-W ∈ P ⟶ Type
6. par : P
7. a : A[par]
8. f : b:B[par;a] ⟶ (pW C[par;a;b])
9. pW-sup(a;f) ∈ pco-W par
10. path : Path
11. StepAgree(path 0;par;pW-sup(a;f))
⊢ ↓∃n:ℕ. Barred(pcw-partial(path;n))

---

Latex:

---

Latex:

1.  P  :  Type
2.  A  :  P  {}\mrightarrow{}  Type
3.  B  :  p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type
4.  C  :  p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P
5.  pco-W  \mmember{}  P  {}\mrightarrow{}  Type
6.  par  :  P
7.  a  :  A[par]
8.  f  :  b:B[par;a]  {}\mrightarrow{}  (pW  C[par;a;b])
\mvdash{}  pW-sup(a;f)  \mmember{}  pW  par


By

---

Latex:
TACTIC:((Assert  pW-sup(a;f)  \mmember{}  pco-W  par  BY
                              (pcoWD  0
                                THEN  Auto
                                THEN  ProveWfLemma
                                THEN  (ExtWith  [`b']  [b:B[par;a]  {}\mrightarrow{}  (pW  C[par;a;b])]\mcdot{}
                                            THEN  Auto
                                            THEN  DoSubsume
                                            THEN  Auto
                                            THEN  (Unfold  `param-W`  0  THEN  Reduce  0)
                                            THEN  Auto)\mcdot{}))
                THEN  (Unfold  `param-W`  0  THEN  Reduce  0  THEN  MemTypeCD  THEN  Auto)\mcdot{}
                )

---

Home Index