---

Step * 1 1 1 1 2 1 1 1 of Lemma pcw-pp-lemma


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. s : pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
6. p1 : P
⊢ pco-W p1 ∈ 𝕌'
BY
{ (InstLemma `param-co-W_wf` [⌜P⌝;⌜A⌝;⌜B⌝;⌜C⌝]⋅ THEN Auto)⋅ }

---

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.  s  :  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
6.  p1  :  P
\mvdash{}  pco-W  p1  \mmember{}  \mBbbU{}'


By

---

Latex:
(InstLemma  `param-co-W\_wf`  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index