---

Step * of Lemma extend-val_wf

∀[a:formula()]. ∀[v0:{b:formula()| b ⊆ a ∧ (↑pvar?(b))}  ⟶ 𝔹]. ∀[g:{b:formula()| b ⊆ a}  ⟶ 𝔹].  (extend-val(v0;g;a) ∈ \000C𝔹)
BY
{ ((D 0 THENA Auto)
   THEN SimpleDatatypeInduction (-1)
   THEN Unfolds ``extend-val psub`` 0
   THEN Reduce 0
   THEN Try (Fold `psub` 0)
   THEN Auto
   THEN MemTypeCD
   THEN Auto
   THEN RWO "psub-same" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:formula()].  \mforall{}[v0:\{b:formula()|  b  \msubseteq{}  a  \mwedge{}  (\muparrow{}pvar?(b))\}    {}\mrightarrow{}  \mBbbB{}].  \mforall{}[g:\{b:formula()|  b  \msubseteq{}  a\}    {}\mrightarrow{}  \mBbbB{}].
    (extend-val(v0;g;a)  \mmember{}  \mBbbB{})


By

---

Latex:
((D  0  THENA  Auto)
  THEN  SimpleDatatypeInduction  (-1)
  THEN  Unfolds  ``extend-val  psub``  0
  THEN  Reduce  0
  THEN  Try  (Fold  `psub`  0)
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  RWO  "psub-same"  0
  THEN  Auto)

---

Home Index