---

Step * of Lemma pscm-ap-comp-type-sq2

No Annotations
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[s1,s2:Top].  (((A)s2)s1 ~ (A)s2 o s1)
BY
{ (Intros THEN UseWitness ⌜Ax⌝⋅ THEN MemCD THEN RWO  "pscm-ap-comp-type-sq" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[Gamma:ps\_context\{j:l\}(C)].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[s1,s2:Top].
    (((A)s2)s1  \msim{}  (A)s2  o  s1)


By

---

Latex:
(Intros  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  MemCD  THEN  RWO    "pscm-ap-comp-type-sq"  0  THEN  Auto)

---

Home Index