---

Step * of Lemma mFO-dest-atomic_wf

∀[T:Type]. ∀[F:Atom ─→ (ℤ List) ─→ (T?)]. ∀[fmla:mFOL()].  (let nm,vars = dest-atomic(fmla) inF[nm;vars] ∈ T?)
BY
{ (Auto THEN Unfold `mFO-dest-atomic` 0 THEN AutoBoolCase ⌈mFOatomic?(fmla)⌉⋅)⋅ }

---

Latex:


\mforall{}[T:Type].  \mforall{}[F:Atom  {}\mrightarrow{}  (\mBbbZ{}  List)  {}\mrightarrow{}  (T?)].  \mforall{}[fmla:mFOL()].
    (let  nm,vars  =  dest-atomic(fmla)  in
      F[nm;vars]  \mmember{}  T?)


By

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

---

Home Index