---

Step * of Lemma typed-cc-fst_wf

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢ _}].  (tp{i:l} ∈ G.A ij⟶ G)
BY
{ PresheafMLTTInstance Obid: typed-psc-fst_wf⋅ }

---

Latex:

---

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


By

---

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

---

Home Index