---

Step * of Lemma W-subtype-coW

∀[A:𝕌']. ∀[B:A ⟶ Type].  (W(A;a.B[a]) ⊆r coW(A;a.B[a]))
BY
{ (TACTIC:Auto THEN (D 0 THENA Auto) THEN RepUR ``W param-W`` -1 THEN D -1) }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. x : pco-W ⋅@i'
4. ∀path:Path. (StepAgree(path 0;⋅;x) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
⊢ x ∈ coW(A;a.B[a])

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].    (W(A;a.B[a])  \msubseteq{}r  coW(A;a.B[a]))


By

---

Latex:
(TACTIC:Auto  THEN  (D  0  THENA  Auto)  THEN  RepUR  ``W  param-W``  -1  THEN  D  -1)

---

Home Index