---

Step * of Lemma mFO-dest-connective_wf

∀[T:Type]. ∀[F:mFOL() ─→ mFOL() ─→ (T?)]. ∀[fmla:mFOL()]. ∀[knd:Atom].  (let a,b = dest-knd(fmla) in F[a;b] ∈ T?)
BY
{ (Auto THEN Unfold `mFO-dest-connective` 0 THEN AutoBoolCase ⌈mFOconnect?(fmla)⌉⋅)⋅ }

---

Latex:


\mforall{}[T:Type].  \mforall{}[F:mFOL()  {}\mrightarrow{}  mFOL()  {}\mrightarrow{}  (T?)].  \mforall{}[fmla:mFOL()].  \mforall{}[knd:Atom].
    (let  a,b  =  dest-knd(fmla)  in
      F[a;b]  \mmember{}  T?)


By

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

---

Home Index