---

Step * of Lemma pscm-ap-type-fst-id-adjoin

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[B:{X ⊢ _}]. ∀[u:Top].  (((B)p)[u] = B ∈ {X ⊢ _})
BY
{ ((Intros THEN Unfold `pscm-id-adjoin` 0) THEN RWO  "pscm-ap-type-fst-adjoin" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[B:\{X  \mvdash{}  \_\}].  \mforall{}[u:Top].    (((B)p)[u]  =  B)


By

---

Latex:
((Intros  THEN  Unfold  `pscm-id-adjoin`  0)  THEN  RWO    "pscm-ap-type-fst-adjoin"  0  THEN  Auto)

---

Home Index