---

Step * of Lemma mFO-dest-quantifier_wf

∀[T:Type]. ∀[F:ℤ ─→ mFOL() ─→ (T?)]. ∀[fmla:mFOL()]. ∀[isall:𝔹].
  (let v,b = dest-if isall then all else exists(fmla); in
    F[v;b] ∈ T?)
BY
{ (Auto THEN Unfold `mFO-dest-quantifier` 0 THEN AutoBoolCase ⌈mFOquant?(fmla)⌉⋅)⋅ }

---

Latex:


\mforall{}[T:Type].  \mforall{}[F:\mBbbZ{}  {}\mrightarrow{}  mFOL()  {}\mrightarrow{}  (T?)].  \mforall{}[fmla:mFOL()].  \mforall{}[isall:\mBbbB{}].
    (let  v,b  =  dest-if  isall  then  all  else  exists(fmla);  in
        F[v;b]  \mmember{}  T?)


By

(Auto  THEN  Unfold  `mFO-dest-quantifier`  0  THEN  AutoBoolCase  \mkleeneopen{}mFOquant?(fmla)\mkleeneclose{}\mcdot{})\mcdot{}

---

Home Index