---

Step * of Lemma pscm-adjoin-fst-snd

No Annotations
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢ _}].
  ((p;q) = 1(Gamma.A) ∈ psc_map{[i | j]:l}(C; Gamma.A; Gamma.A))
BY
{ (Auto
   THEN Symmetry
   THEN BLemma `pscm-equal`
   THEN Try (Complete (Auto))
   THEN RepeatFor 2 (DVar `A')
   THEN (RepUR ``pscm-adjoin psc-fst psc-snd I_set psc-adjoin pscm-ap pscm-id`` 0 THEN RepUR ``functor-ob`` 0)
   THEN (Fold `functor-ob` 0 THEN Fold `I_set` 0)
   THEN Auto
   THEN RepeatFor 2 ((Ext THENA Auto))
   THEN Reduce 0
   THEN (D -1 THEN RepUR ``functor-ob`` 0)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Symmetry
  THEN  BLemma  `pscm-equal`
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  2  (DVar  `A')
  THEN  (RepUR  ``pscm-adjoin  psc-fst  psc-snd  I\_set  psc-adjoin  pscm-ap  pscm-id``  0
              THEN  RepUR  ``functor-ob``  0
              )
  THEN  (Fold  `functor-ob`  0  THEN  Fold  `I\_set`  0)
  THEN  Auto
  THEN  RepeatFor  2  ((Ext  THENA  Auto))
  THEN  Reduce  0
  THEN  (D  -1  THEN  RepUR  ``functor-ob``  0)
  THEN  Auto)

---

Home Index