---

Step * of Lemma typed-cc-snd_wf

No Annotations
∀G:j⊢. ∀A:{G ⊢ _}.  (tq ∈ {G.A ⊢ _:(A)tp{i:l}})
BY
{ PresheafMLTTInstance Obid: typed-psc-snd_wf⋅ }

---

Latex:

---

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


By

---

Latex:
PresheafMLTTInstance  Obid:  typed-psc-snd\_wf\mcdot{}

---

Home Index