---

Step * of Lemma pscm-ap-type-is-id

No Annotations
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[s:psc_map{j:l}(C; Gamma; Gamma)].
  (A)s = A ∈ {Gamma ⊢ _} supposing s = 1(Gamma) ∈ psc_map{j:l}(C; Gamma; Gamma)
BY
{ (Auto THEN HypSubst' (-1) 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[Gamma:ps\_context\{j:l\}(C)].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].
\mforall{}[s:psc\_map\{j:l\}(C;  Gamma;  Gamma)].
    (A)s  =  A  supposing  s  =  1(Gamma)


By

---

Latex:
(Auto  THEN  HypSubst'  (-1)  0  THEN  Auto)

---

Home Index