---

Step * of Lemma psc-snd-pscm-adjoin

No Annotations
∀[C:SmallCategory]. ∀[Gamma,Delta:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}]. ∀[sigma:psc_map{j:l}(C; Delta; Gamma)].
∀[u:{Delta ⊢ _:(A)sigma}].
  ((q)(sigma;u) = u ∈ {Delta ⊢ _:(A)sigma})
BY
{ (Auto THEN (InstLemma `psc-snd-pscm-adjoin-sq` [⌜Delta⌝]⋅ THENA Auto) THEN RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[Gamma,Delta:ps\_context\{j:l\}(C)].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[sigma:psc\_map\{j:l\}(C;
                                                                                                                                                                                            Delta;
                                                                                                                                                                                            Gamma
                                                                                                                                                                                            )].
\mforall{}[u:\{Delta  \mvdash{}  \_:(A)sigma\}].
    ((q)(sigma;u)  =  u)


By

---

Latex:
(Auto  THEN  (InstLemma  `psc-snd-pscm-adjoin-sq`  [\mkleeneopen{}Delta\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RWO  "-1"  0  THEN  Auto)

---

Home Index