---

Step * of Lemma context-lookup_wf

∀[Gamma:mFOL() List]. ∀[x:ℕ||Gamma||].  (context-lookup(Gamma;x) ∈ mFOL())
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[Gamma:mFOL()  List].  \mforall{}[x:\mBbbN{}||Gamma||].    (context-lookup(Gamma;x)  \mmember{}  mFOL())


By

---

Latex:
ProveWfLemma

---

Home Index