Step
*
1
2
of Lemma
coW-equiv-iff2
1. [A] : π'
2. B : A βΆ Type
3. n : β€
4. [%1] : 0 < n
5. βw,w':coW(A;a.B[a]).
(coW-equiv(a.B[a];w;w')
β (βp1:coPath(a.B[a];w';n - 1)
βq:copath(a.B[a];w)
((copath-length(q) = (n - 1) β β€) β§ coW-equiv(a.B[a];coPath-at(n - 1;w';p1);copath-at(w;q)))))
6. w : coW(A;a.B[a])
7. w' : coW(A;a.B[a])
8. coW-equiv(a.B[a];w;w')
9. p1 : coPath(a.B[a];w';n)
β’ βq:copath(a.B[a];w). ((copath-length(q) = n β β€) β§ coW-equiv(a.B[a];coPath-at(n;w';p1);copath-at(w;q)))
BY
{ (Unfold `coPath` -1
THEN (SplitOnHypITE -1 THENA Auto)
THEN Try ((Assert βFalseββ
THEN Complete (Auto)))
THEN Thin (-1)
THEN D -1) }
1
1. [A] : π'
2. B : A βΆ Type
3. n : β€
4. [%1] : 0 < n
5. βw,w':coW(A;a.B[a]).
(coW-equiv(a.B[a];w;w')
β (βp1:coPath(a.B[a];w';n - 1)
βq:copath(a.B[a];w)
((copath-length(q) = (n - 1) β β€) β§ coW-equiv(a.B[a];coPath-at(n - 1;w';p1);copath-at(w;q)))))
6. w : coW(A;a.B[a])
7. w' : coW(A;a.B[a])
8. coW-equiv(a.B[a];w;w')
9. t : coW-dom(a.B[a];w')
10. p2 : coPath(a.B[a];coW-item(w';t);n - 1)
β’ βq:copath(a.B[a];w). ((copath-length(q) = n β β€) β§ coW-equiv(a.B[a];coPath-at(n;w';<t, p2>);copath-at(w;q)))
Latex:
Latex:
1. [A] : \mBbbU{}'
2. B : A {}\mrightarrow{} Type
3. n : \mBbbZ{}
4. [\%1] : 0 < n
5. \mforall{}w,w':coW(A;a.B[a]).
(coW-equiv(a.B[a];w;w')
{}\mRightarrow{} (\mforall{}p1:coPath(a.B[a];w';n - 1)
\mexists{}q:copath(a.B[a];w)
((copath-length(q) = (n - 1))
\mwedge{} coW-equiv(a.B[a];coPath-at(n - 1;w';p1);copath-at(w;q)))))
6. w : coW(A;a.B[a])
7. w' : coW(A;a.B[a])
8. coW-equiv(a.B[a];w;w')
9. p1 : coPath(a.B[a];w';n)
\mvdash{} \mexists{}q:copath(a.B[a];w)
((copath-length(q) = n) \mwedge{} coW-equiv(a.B[a];coPath-at(n;w';p1);copath-at(w;q)))
By
Latex:
(Unfold `coPath` -1
THEN (SplitOnHypITE -1 THENA Auto)
THEN Try ((Assert \mkleeneopen{}False\mkleeneclose{}\mcdot{} THEN Complete (Auto)))
THEN Thin (-1)
THEN D -1)
Home
Index