---

Step * of Lemma copath-last_wf

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)].
  copath-last(w;p) ∈ w':coW(A;a.B[a]) × coW-dom(a.B[a];w') supposing 0 < copath-length(p)
BY
{ (Auto
   THEN (Assert ∀n:ℕ. ∀w:coW(A;a.B[a]). ∀p:copath(a.B[a];w).
                  (0 < copath-length(p)
                  ⇒ (copath-length(p) ≤ n)
                  ⇒ (copath-last(w;p) ∈ w':coW(A;a.B[a]) × coW-dom(a.B[a];w'))) BY
               ((InductionOnNat THEN Auto)
                THEN Unfold `copath-last` 0
                THEN AutoSplit
                THEN BackThruSomeHyp
                THEN RWO "length-copath-tl" 0
                THEN Auto))
   THEN InstHyp [⌜copath-length(p)⌝;⌜w⌝;⌜p⌝] (-1)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w:coW(A;a.B[a])].  \mforall{}[p:copath(a.B[a];w)].
    copath-last(w;p)  \mmember{}  w':coW(A;a.B[a])  \mtimes{}  coW-dom(a.B[a];w')  supposing  0  <  copath-length(p)


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}n:\mBbbN{}.  \mforall{}w:coW(A;a.B[a]).  \mforall{}p:copath(a.B[a];w).
                                (0  <  copath-length(p)
                                {}\mRightarrow{}  (copath-length(p)  \mleq{}  n)
                                {}\mRightarrow{}  (copath-last(w;p)  \mmember{}  w':coW(A;a.B[a])  \mtimes{}  coW-dom(a.B[a];w')))  BY
                          ((InductionOnNat  THEN  Auto)
                            THEN  Unfold  `copath-last`  0
                            THEN  AutoSplit
                            THEN  BackThruSomeHyp
                            THEN  RWO  "length-copath-tl"  0
                            THEN  Auto))
  THEN  InstHyp  [\mkleeneopen{}copath-length(p)\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto)

---

Home Index