---

Step * of Lemma valuation-val

∀[z:formula()]. ∀[v0:{a:formula()| a ⊆ z ∧ (↑pvar?(a))}  ⟶ 𝔹]. ∀[f:{f:{a:formula()| a ⊆ z}  ⟶ 𝔹| valuation(v0;z;f)} ].
  f z = extend-val(v0;f;z)
BY
{ ((Auto THEN DVar `f')
   THEN Unfold `valuation` (-1)
   THEN BHyp -1 
   THEN Auto
   THEN MemTypeCD
   THEN Auto
   THEN BLemma `psub_weakening` 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[z:formula()].  \mforall{}[v0:\{a:formula()|  a  \msubseteq{}  z  \mwedge{}  (\muparrow{}pvar?(a))\}    {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{f:\{a:formula()|  a  \msubseteq{}  z\}    {}\mrightarrow{}  \mBbbB{}| 
                                                                                                                                        valuation(v0;z;f)\}  ].
    f  z  =  extend-val(v0;f;z)


By

---

Latex:
((Auto  THEN  DVar  `f')
  THEN  Unfold  `valuation`  (-1)
  THEN  BHyp  -1 
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  BLemma  `psub\_weakening` 
  THEN  Auto)

---

Home Index