---

Step * of Lemma copathAgree-last

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p,q:copath(a.B[a];w)].
  (((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
     ∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))) supposing 
     ((copath-length(q) = (copath-length(p) + 1) ∈ ℤ) and 
     copathAgree(a.B[a];w;p;q))
BY
{ (RepeatFor 2 (Intro)
   THEN (Assert ⌜∀n:ℕ
                   ∀[w:coW(A;a.B[a])]. ∀[p,q:copath(a.B[a];w)].
                     (((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
                        ∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))) supposing 
                        ((copath-length(q) = (copath-length(p) + 1) ∈ ℤ) and 
                        copathAgree(a.B[a];w;p;q) and 
                        (copath-length(q) ≤ n))⌝⋅
        THENM (Auto THEN D 3 With ⌜copath-length(q)⌝  THEN Auto)
        )
   ) }

1
.....assertion..... 
1. [A] : 𝕌'
2. [B] : A ⟶ Type
⊢ ∀n:ℕ
    ∀[w:coW(A;a.B[a])]. ∀[p,q:copath(a.B[a];w)].
      (((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
         ∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))) supposing 
         ((copath-length(q) = (copath-length(p) + 1) ∈ ℤ) and 
         copathAgree(a.B[a];w;p;q) and 
         (copath-length(q) ≤ n))

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w:coW(A;a.B[a])].  \mforall{}[p,q:copath(a.B[a];w)].
    (((fst(copath-last(w;q)))  =  copath-at(w;p))
          \mwedge{}  (copath-at(w;q)  =  coW-item(copath-at(w;p);snd(copath-last(w;q)))))  supposing 
          ((copath-length(q)  =  (copath-length(p)  +  1))  and 
          copathAgree(a.B[a];w;p;q))


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  (Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}
                                  \mforall{}[w:coW(A;a.B[a])].  \mforall{}[p,q:copath(a.B[a];w)].
                                      (((fst(copath-last(w;q)))  =  copath-at(w;p))
                                            \mwedge{}  (copath-at(w;q)
                                                =  coW-item(copath-at(w;p);snd(copath-last(w;q)))))  supposing 
                                            ((copath-length(q)  =  (copath-length(p)  +  1))  and 
                                            copathAgree(a.B[a];w;p;q)  and 
                                            (copath-length(q)  \mleq{}  n))\mkleeneclose{}\mcdot{}
            THENM  (Auto  THEN  D  3  With  \mkleeneopen{}copath-length(q)\mkleeneclose{}    THEN  Auto)
            )
  )

---

Home Index