---

Step * 1 of Lemma copath-at-extend

.....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))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN D -1
   THEN Reduce 0
   THEN (InstHyp [⌜coW-item(w;t)⌝;⌜p2⌝] 5⋅ THENA Auto)
   THEN ParallelLast
   THEN NthHypSq (-1)
   THEN Auto) }

---

Latex:

---

Latex:
.....falsecase..... 
1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  \mforall{}w:coW(A;a.B[a]).  \mforall{}p1:coPath(a.B[a];w;n  -  1).  \mforall{}t:Top.
          (coPath-at((n  -  1)  +  1;w;coPath-extend(n  -  1;p1;t))  \msim{}  coW-item(coPath-at(n  -  1;w;p1);t))
6.  \mneg{}(n  =  0)
7.  \mneg{}((n  +  1)  =  0)
\mvdash{}  \mforall{}w:coW(A;a.B[a]).  \mforall{}p1:t:coW-dom(a.B[a];w)  \mtimes{}  coPath(a.B[a];coW-item(w;t);n  -  1).  \mforall{}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)  \msim{}  coW-item(let  t,q  =  p1 
                                                                                                                    in  coPath-at(n  -  1;coW-item(w;t);q);t))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  D  -1
  THEN  Reduce  0
  THEN  (InstHyp  [\mkleeneopen{}coW-item(w;t)\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  NthHypSq  (-1)
  THEN  Auto)

---

Home Index