---

Step * of Lemma csm-path-type-sub-pathtype

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[H:j⊢]. ∀[tau:H j⟶ X].  ({H ⊢ _:((Path_A a b))tau} ⊆r {H ⊢ _:(Path(A))tau})
BY
{ (Auto THEN RWO "csm-path-type csm-pathtype" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[H:j\mvdash{}].  \mforall{}[tau:H  j{}\mrightarrow{}  X].
    (\{H  \mvdash{}  \_:((Path\_A  a  b))tau\}  \msubseteq{}r  \{H  \mvdash{}  \_:(Path(A))tau\})


By

---

Latex:
(Auto  THEN  RWO  "csm-path-type  csm-pathtype"  0  THEN  Auto)

---

Home Index