---

Step * of Lemma coW-equiv_transitivity

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w1,w2,w3:coW(A;a.B[a])].
  (coW-equiv(a.B[a];w1;w2) ⇒ coW-equiv(a.B[a];w2;w3) ⇒ coW-equiv(a.B[a];w1;w3))
BY
{ (Auto
   THEN All (Unfold `coW-equiv`)
   THEN All (Unfold `win2`)
   THEN ParallelOp -2
   THEN (D -3 With ⌜n⌝  THENA Auto)
   THEN RenameVar `X' (-2)
   THEN RenameVar `Y' (-1)
   THEN UseWitness ⌜coW-trans(X; Y)⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w1,w2,w3:coW(A;a.B[a])].
    (coW-equiv(a.B[a];w1;w2)  {}\mRightarrow{}  coW-equiv(a.B[a];w2;w3)  {}\mRightarrow{}  coW-equiv(a.B[a];w1;w3))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `coW-equiv`)
  THEN  All  (Unfold  `win2`)
  THEN  ParallelOp  -2
  THEN  (D  -3  With  \mkleeneopen{}n\mkleeneclose{}    THENA  Auto)
  THEN  RenameVar  `X'  (-2)
  THEN  RenameVar  `Y'  (-1)
  THEN  UseWitness  \mkleeneopen{}coW-trans(X;  Y)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index