---

Step * of Lemma typed-psc-snd_wf

No Annotations
∀C:SmallCategory. ∀G:ps_context{j:l}(C). ∀A:{G ⊢ _}.  (tq ∈ {G.A ⊢ _:(A)tp{i:l}})
BY
{ (Intros THEN Unfold `typed-psc-fst` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}C:SmallCategory.  \mforall{}G:ps\_context\{j:l\}(C).  \mforall{}A:\{G  \mvdash{}  \_\}.    (tq  \mmember{}  \{G.A  \mvdash{}  \_:(A)tp\{i:l\}\})


By

---

Latex:
(Intros  THEN  Unfold  `typed-psc-fst`  0  THEN  ProveWfLemma)

---

Home Index