---

Step * 1 of Lemma equal-implies-member-param-W


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. w : pco-W p
8. ∀path:Path. (StepAgree(path 0;p;w) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
9. w' : pco-W p
10. w = w' ∈ (pco-W p)
11. path : Path
12. StepAgree(path 0;p;w')
⊢ StepAgree(path 0;p;w)
BY
{ (NthHypEq (-1) THEN At ⌜𝕌'⌝EqCD⋅ THEN Auto THEN 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.  pco-W  \mmember{}  P  {}\mrightarrow{}  Type
6.  p  :  P
7.  w  :  pco-W  p
8.  \mforall{}path:Path.  (StepAgree(path  0;p;w)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}n:\mBbbN{}.  Barred(pcw-partial(path;n))))
9.  w'  :  pco-W  p
10.  w  =  w'
11.  path  :  Path
12.  StepAgree(path  0;p;w')
\mvdash{}  StepAgree(path  0;p;w)


By

---

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

---

Home Index