---

Step * of Lemma copath-at-extend

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[p:copath(a.B[a];w)]. ∀[t:Top].
  (copath-at(w;copath-extend(p;t)) ~ coW-item(copath-at(w;p);t))
BY
{ (Auto
   THEN D -2
   THEN RepUR ``copath-at`` 0
   THEN RepUR ``copath-at`` -1
   THEN MoveToConcl (-1)
   THEN MoveToConcl 3
   THEN NatInd (-1)
   THEN Unfold `coPath` 0
   THEN Unfold `coPath-at` 0
   THEN Unfold `coPath-extend` 0
   THEN Reduce 0
   THEN (RepeatFor 2 (((SplitOnConclITE THENA Auto) THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))))
   ORELSE ((Unfold `coPath-at` 0 THEN Reduce 0) THEN Auto)
   )) }

1
.....falsecase..... 
1. A : 𝕌'
2. B : A ⟶ Type
3. n : ℤ
4. 0 < n
5. ∀w:coW(A;a.B[a]). ∀p1:coPath(a.B[a];w;n - 1). ∀t:Top.
     (coPath-at((n - 1) + 1;w;coPath-extend(n - 1;p1;t)) ~ coW-item(coPath-at(n - 1;w;p1);t))
6. ¬(n = 0 ∈ ℤ)
7. ¬((n + 1) = 0 ∈ ℤ)
⊢ ∀w:coW(A;a.B[a]). ∀p1:t:coW-dom(a.B[a];w) × coPath(a.B[a];coW-item(w;t);n - 1). ∀t:Top.
    (let t,q = let x,y = p1 
               in <x, coPath-extend(n - 1;y;t)> 
     in coPath-at((n + 1) - 1;coW-item(w;t);q) ~ coW-item(let t,q = p1 
                                                          in coPath-at(n - 1;coW-item(w;t);q);t))

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w:coW(A;a.B[a])].  \mforall{}[p:copath(a.B[a];w)].  \mforall{}[t:Top].
    (copath-at(w;copath-extend(p;t))  \msim{}  coW-item(copath-at(w;p);t))


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  RepUR  ``copath-at``  0
  THEN  RepUR  ``copath-at``  -1
  THEN  MoveToConcl  (-1)
  THEN  MoveToConcl  3
  THEN  NatInd  (-1)
  THEN  Unfold  `coPath`  0
  THEN  Unfold  `coPath-at`  0
  THEN  Unfold  `coPath-extend`  0
  THEN  Reduce  0
  THEN  (RepeatFor  2  (((SplitOnConclITE  THENA  Auto)
                                          THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto)))
                                          ))
  ORELSE  ((Unfold  `coPath-at`  0  THEN  Reduce  0)  THEN  Auto)
  ))

---

Home Index