---

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

∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[p:P]. ∀[w:pW p].
∀[w':pco-W p].
  w' ∈ pW p supposing w = w' ∈ (pco-W p)
BY
{ (InstLemma `param-co-W_wf` []⋅
   THEN RepeatFor 4 (ParallelLast')
   THEN Auto
   THEN All (RepUR ``param-W``)
   THEN Auto
   THEN D (-3)
   THEN MemTypeCD
   THEN Auto
   THEN BackThruSomeHyp) }

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. 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)

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[A:P  {}\mrightarrow{}  Type].  \mforall{}[B:p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type].  \mforall{}[C:p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P].  \mforall{}[p:P].
\mforall{}[w:pW  p].  \mforall{}[w':pco-W  p].
    w'  \mmember{}  pW  p  supposing  w  =  w'


By

---

Latex:
(InstLemma  `param-co-W\_wf`  []\mcdot{}
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto
  THEN  All  (RepUR  ``param-W``)
  THEN  Auto
  THEN  D  (-3)
  THEN  MemTypeCD
  THEN  Auto
  THEN  BackThruSomeHyp)

---

Home Index