---

Step * 1 1 of Lemma param-W-ext


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. p : P
7. a : A[p]
8. x1 : b:B[p;a] ⟶ (pco-W C[p;a;b])
9. ∀path:Path. (StepAgree(path 0;p;<a, x1>) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
10. <a, x1> ∈ pco-W p
⊢ x1 ∈ b:B[p;a] ⟶ (pW C[p;a;b])
BY
{ ((ExtWith [`b'] [⌜b:B[p;a] ⟶ (pco-W C[p;a;b])⌝]⋅ THENA Auto) THEN RepUR ``param-W`` 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. p : P
7. a : A[p]
8. x1 : b:B[p;a] ⟶ (pco-W C[p;a;b])
9. ∀path:Path. (StepAgree(path 0;p;<a, x1>) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
10. <a, x1> ∈ pco-W p
11. b : B[p;a]
12. path : Path
13. StepAgree(path 0;C[p;a;b];x1 b)
⊢ ↓∃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.  p  :  P
7.  a  :  A[p]
8.  x1  :  b:B[p;a]  {}\mrightarrow{}  (pco-W  C[p;a;b])
9.  \mforall{}path:Path.  (StepAgree(path  0;p;<a,  x1>)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}n:\mBbbN{}.  Barred(pcw-partial(path;n))))
10.  <a,  x1>  \mmember{}  pco-W  p
\mvdash{}  x1  \mmember{}  b:B[p;a]  {}\mrightarrow{}  (pW  C[p;a;b])


By

---

Latex:
((ExtWith  [`b']  [\mkleeneopen{}b:B[p;a]  {}\mrightarrow{}  (pco-W  C[p;a;b])\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``param-W``  0
  THEN  MemTypeCD
  THEN  Auto)\mcdot{}

---

Home Index