---

Step * of Lemma coPathAgree_wf

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[n:ℕ]. ∀[w:coW(A;a.B[a])]. ∀[p,q:coPath(a.B[a];w;n)].  (coPathAgree(a.B[a];n;w;p;q) ∈ ℙ)
BY
{ (InductionOnNat THEN Auto THEN Unfold `coPathAgree` 0 THEN AutoSplit) }

1
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') ∈ ℙ

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[w:coW(A;a.B[a])].  \mforall{}[p,q:coPath(a.B[a];w;n)].
    (coPathAgree(a.B[a];n;w;p;q)  \mmember{}  \mBbbP{})


By

---

Latex:
(InductionOnNat  THEN  Auto  THEN  Unfold  `coPathAgree`  0  THEN  AutoSplit)

---

Home Index