---

Step * of Lemma pscm+_wf

No Annotations
∀[C:SmallCategory]. ∀[H,K:ps_context{j:l}(C)]. ∀[A:{H ⊢ _}]. ∀[tau:psc_map{j:l}(C; K; H)].
  (tau+ ∈ psc_map{[i | j]:l}(C; K.(A)tau; H.A))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[H,K:ps\_context\{j:l\}(C)].  \mforall{}[A:\{H  \mvdash{}  \_\}].  \mforall{}[tau:psc\_map\{j:l\}(C;  K;  H)].
    (tau+  \mmember{}  psc\_map\{[i  |  j]:l\}(C;  K.(A)tau;  H.A))


By

---

Latex:
ProveWfLemma

---

Home Index