---

Step * of Lemma copathAgree-cons

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])]. ∀[b:coW-dom(a.B[a];w)].
  ∀p,q:copath(a.B[a];coW-item(w;b)).
    (copathAgree(a.B[a];coW-item(w;b);p;q) ⇒ copathAgree(a.B[a];w;copath-cons(b;p);copath-cons(b;q)))
BY
{ (Auto
   THEN D -3
   THEN D -2
   THEN ParallelLast
   THEN All Reduce
   THEN (Decide ⌜n < n1⌝⋅ THENA Auto)
   THEN All Reduce
   THEN Auto
   THEN AutoSplit) }

1
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. [w] : coW(A;a.B[a])
4. [b] : coW-dom(a.B[a];w)
5. n : ℕ
6. p1 : coPath(a.B[a];coW-item(w;b);n)
7. n1 : ℕ
8. q1 : coPath(a.B[a];coW-item(w;b);n1)
9. coPathAgree(a.B[a];n;coW-item(w;b);p1;q1)
10. n < n1
11. n + 1 < n1 + 1
⊢ coPathAgree(a.B[a];n + 1;w;<b, p1>;<b, q1>)

2
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. [w] : coW(A;a.B[a])
4. [b] : coW-dom(a.B[a];w)
5. n : ℕ
6. p1 : coPath(a.B[a];coW-item(w;b);n)
7. n1 : ℕ
8. ¬n + 1 < n1 + 1
9. q1 : coPath(a.B[a];coW-item(w;b);n1)
10. coPathAgree(a.B[a];n1;coW-item(w;b);p1;q1)
11. ¬n < n1
⊢ coPathAgree(a.B[a];n1 + 1;w;<b, p1>;<b, q1>)

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w:coW(A;a.B[a])].  \mforall{}[b:coW-dom(a.B[a];w)].
    \mforall{}p,q:copath(a.B[a];coW-item(w;b)).
        (copathAgree(a.B[a];coW-item(w;b);p;q)
        {}\mRightarrow{}  copathAgree(a.B[a];w;copath-cons(b;p);copath-cons(b;q)))


By

---

Latex:
(Auto
  THEN  D  -3
  THEN  D  -2
  THEN  ParallelLast
  THEN  All  Reduce
  THEN  (Decide  \mkleeneopen{}n  <  n1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Reduce
  THEN  Auto
  THEN  AutoSplit)

---

Home Index