---

Step * of Lemma copath-at-W

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w:W(A;a.B[a])]. ∀[p:copath(a.B[a];w)].  (copath-at(w;p) ∈ W(A;a.B[a]))
BY
{ (RepeatFor 2 (Intro)
   THEN (Assert W(A;a.B[a]) ⊆r coW(A;a.B[a]) BY
               Auto)
   THEN Intro
   THEN (InstLemma `copath_wf` [⌜A⌝;⌜B⌝;⌜w⌝]⋅ THENA Auto)
   THEN Intro
   THEN Unhide
   THEN D -1
   THEN RepUR ``copath-at`` 0) }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. W(A;a.B[a]) ⊆r coW(A;a.B[a])
4. w : W(A;a.B[a])
5. copath(a.B[a];w) ∈ Type
6. n : ℕ
7. p1 : coPath(a.B[a];w;n)
⊢ coPath-at(n;w;p1) ∈ W(A;a.B[a])

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w:W(A;a.B[a])].  \mforall{}[p:copath(a.B[a];w)].    (copath-at(w;p)  \mmember{}  W(A;a.B[a]))


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  (Assert  W(A;a.B[a])  \msubseteq{}r  coW(A;a.B[a])  BY
                          Auto)
  THEN  Intro
  THEN  (InstLemma  `copath\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Intro
  THEN  Unhide
  THEN  D  -1
  THEN  RepUR  ``copath-at``  0)

---

Home Index