---

Step * of Lemma pscm-id_wf

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)].  (1(X) ∈ psc_map{j:l}(C; X; X))
BY
{ ((Auto THEN (RWO "pscm-id-sq" 0 THENA Auto))
   THEN Unfolds ``psc_map`` 0
   THEN ∀h:hyp. Unfold `ps_context` h 
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].    (1(X)  \mmember{}  psc\_map\{j:l\}(C;  X;  X))


By

---

Latex:
((Auto  THEN  (RWO  "pscm-id-sq"  0  THENA  Auto))
  THEN  Unfolds  ``psc\_map``  0
  THEN  \mforall{}h:hyp.  Unfold  `ps\_context`  h 
  THEN  Auto)

---

Home Index