---

Step * 1 of Lemma coPathAgree_wf


1. A : 𝕌'
2. B : A ⟶ Type
3. n : ℤ
4. n ≠ 0
5. 0 < n
6. ∀[w:coW(A;a.B[a])]. ∀[p,q:coPath(a.B[a];w;n - 1)].  (coPathAgree(a.B[a];n - 1;w;p;q) ∈ ℙ)
7. w : coW(A;a.B[a])
8. p : coPath(a.B[a];w;n)
9. q : coPath(a.B[a];w;n)
⊢ let t,p' = p 
  in let t',q' = q 
     in (t = t' ∈ coW-dom(a.B[a];w)) ∧ coPathAgree(a.B[a];n - 1;coW-item(w;t);p';q') ∈ ℙ
BY
{ RepeatFor 2 ((Unfold `coPath` -2 THEN SplitOnHypITE -2  THEN Auto)) }

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  n  :  \mBbbZ{}
4.  n  \mneq{}  0
5.  0  <  n
6.  \mforall{}[w:coW(A;a.B[a])].  \mforall{}[p,q:coPath(a.B[a];w;n  -  1)].    (coPathAgree(a.B[a];n  -  1;w;p;q)  \mmember{}  \mBbbP{})
7.  w  :  coW(A;a.B[a])
8.  p  :  coPath(a.B[a];w;n)
9.  q  :  coPath(a.B[a];w;n)
\mvdash{}  let  t,p'  =  p 
    in  let  t',q'  =  q 
          in  (t  =  t')  \mwedge{}  coPathAgree(a.B[a];n  -  1;coW-item(w;t);p';q')  \mmember{}  \mBbbP{}


By

---

Latex:
RepeatFor  2  ((Unfold  `coPath`  -2  THEN  SplitOnHypITE  -2    THEN  Auto))

---

Home Index