---

Step * of Lemma coPathAgree_le

∀[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) ⇒ (∀m:ℕ. ((m ≤ n) ⇒ coPathAgree(a.B[a];m;w;p;q))))
BY
{ (InductionOnNat THENA Auto) }

1
.....basecase..... 
1. [A] : 𝕌'
2. [B] : A ⟶ Type
⊢ ∀[w:coW(A;a.B[a])]
    ∀p,q:coPath(a.B[a];w;0).  (coPathAgree(a.B[a];0;w;p;q) ⇒ (∀m:ℕ. ((m ≤ 0) ⇒ coPathAgree(a.B[a];m;w;p;q))))

2
.....upcase..... 
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. n : ℤ
4. [%1] : 0 < n
5. ∀[w:coW(A;a.B[a])]
     ∀p,q:coPath(a.B[a];w;n - 1).
       (coPathAgree(a.B[a];n - 1;w;p;q) ⇒ (∀m:ℕ. ((m ≤ (n - 1)) ⇒ coPathAgree(a.B[a];m;w;p;q))))
⊢ ∀[w:coW(A;a.B[a])]
    ∀p,q:coPath(a.B[a];w;n).  (coPathAgree(a.B[a];n;w;p;q) ⇒ (∀m:ℕ. ((m ≤ n) ⇒ coPathAgree(a.B[a];m;w;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)  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  ((m  \mleq{}  n)  {}\mRightarrow{}  coPathAgree(a.B[a];m;w;p;q))))


By

---

Latex:
(InductionOnNat  THENA  Auto)

---

Home Index