---

Step * of Lemma csm-same-cubical-term

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[u,v:{X ⊢ _:A}]. ∀[Y:j⊢]. ∀[s:Y j⟶ X].  Y ⊢ (u)s=(v)s:(A)s supposing X ⊢ u=v:A
BY
{ (Auto THEN ParallelLast THEN EqCD THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[u,v:\{X  \mvdash{}  \_:A\}].  \mforall{}[Y:j\mvdash{}].  \mforall{}[s:Y  j{}\mrightarrow{}  X].
    Y  \mvdash{}  (u)s=(v)s:(A)s  supposing  X  \mvdash{}  u=v:A


By

---

Latex:
(Auto  THEN  ParallelLast  THEN  EqCD  THEN  Auto)

---

Home Index