---

Step * 1 of Lemma param-W-rel_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. par : P
6. w : pW par
7. n : ℕ
8. ¬0 < n
9. ss : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
10. s : pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
⊢ w ∈ pco-W par
BY
{ (RepUR ``param-W`` 6 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.  par  :  P
6.  w  :  pW  par
7.  n  :  \mBbbN{}
8.  \mneg{}0  <  n
9.  ss  :  \mBbbN{}n  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
10.  s  :  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
\mvdash{}  w  \mmember{}  pco-W  par


By

---

Latex:
(RepUR  ``param-W``  6  THEN  Auto)\mcdot{}

---

Home Index