---

Step * of Lemma coPathAgree_transitivity

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

1
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. n : ℤ
4. n ≠ 0
5. [%1] : 0 < n
6. ∀[w:coW(A;a.B[a])]
     ∀p,q,r:coPath(a.B[a];w;n - 1).
       (coPathAgree(a.B[a];n - 1;w;p;q) ⇒ coPathAgree(a.B[a];n - 1;w;q;r) ⇒ coPathAgree(a.B[a];n - 1;w;p;r))
⊢ ∀[w:coW(A;a.B[a])]
    ∀p,q,r:t:coW-dom(a.B[a];w) × coPath(a.B[a];coW-item(w;t);n - 1).
      (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')
      ⇒ let t,p' = q 
         in let t',q' = r 
            in (t = t' ∈ coW-dom(a.B[a];w)) ∧ coPathAgree(a.B[a];n - 1;coW-item(w;t);p';q')
      ⇒ let t,p' = p 
         in let t',q' = r 
            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,r:coPath(a.B[a];w;n).
                (coPathAgree(a.B[a];n;w;p;q)  {}\mRightarrow{}  coPathAgree(a.B[a];n;w;q;r)  {}\mRightarrow{}  coPathAgree(a.B[a];n;w;p;r))


By

---

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

---

Home Index