---

Step * of Lemma copathAgree-tl

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:coW(A;a.B[a])].
  ∀p,q:copath(a.B[a];w).
    (copathAgree(a.B[a];w;p;q)
    ⇒ 0 < copath-length(p)
    ⇒ 0 < copath-length(q)
    ⇒ copathAgree(a.B[a];coW-item(w;copath-hd(p));copath-tl(p);copath-tl(q)))
BY
{ ((Auto THEN D 5 THEN D 4)
   THEN ParallelOp -3
   THEN All Reduce
   THEN RepUR ``copath-length`` -2
   THEN RepUR ``copath-length`` -1
   THEN (Decide ⌜n1 < n⌝⋅ THENA Auto)
   THEN All Reduce
   THEN Auto
   THEN AutoSplit
   THEN ∀h:hyp. (UnfoldTopAb h THEN (SplitOnHypITE h  THEN Auto) THEN Try (D h)) 
   THEN All Reduce
   THEN Auto) }

---

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).
        (copathAgree(a.B[a];w;p;q)
        {}\mRightarrow{}  0  <  copath-length(p)
        {}\mRightarrow{}  0  <  copath-length(q)
        {}\mRightarrow{}  copathAgree(a.B[a];coW-item(w;copath-hd(p));copath-tl(p);copath-tl(q)))


By

---

Latex:
((Auto  THEN  D  5  THEN  D  4)
  THEN  ParallelOp  -3
  THEN  All  Reduce
  THEN  RepUR  ``copath-length``  -2
  THEN  RepUR  ``copath-length``  -1
  THEN  (Decide  \mkleeneopen{}n1  <  n\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Reduce
  THEN  Auto
  THEN  AutoSplit
  THEN  \mforall{}h:hyp.  (UnfoldTopAb  h  THEN  (SplitOnHypITE  h    THEN  Auto)  THEN  Try  (D  h)) 
  THEN  All  Reduce
  THEN  Auto)

---

Home Index