---

Step * of Lemma peval_wf

∀[x:formula()]. ∀[v0:{a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹].  (peval(v0;x) ∈ 𝔹)
BY
{ ProveWfLemma }

1
1. x : formula()
2. v0 : {a:formula()| a ⊆ x ∧ (↑pvar?(a))}  ⟶ 𝔹
⊢ x ∈ {a:formula()| a ⊆ x} 

---

Latex:

---

Latex:
\mforall{}[x:formula()].  \mforall{}[v0:\{a:formula()|  a  \msubseteq{}  x  \mwedge{}  (\muparrow{}pvar?(a))\}    {}\mrightarrow{}  \mBbbB{}].    (peval(v0;x)  \mmember{}  \mBbbB{})


By

---

Latex:
ProveWfLemma

---

Home Index