---

Step * of Lemma std-env_wf

∀[M:Type ⟶ Type]. ∀[nm:Id].  (std-env(nm) ∈ pEnvType(P.M[P]))
BY
{ (Unfold `pEnvType` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[nm:Id].    (std-env(nm)  \mmember{}  pEnvType(P.M[P]))


By

---

Latex:
(Unfold  `pEnvType`  0  THEN  ProveWfLemma)

---

Home Index