---

Step * of Lemma mFOconnect_wf

∀[knd:Atom]. ∀[left,right:mFOL()].  (mFOconnect(knd;left;right) ∈ mFOL())
BY
{ DepprodCoDatatypeConstructorWf `mFOL_size` }

---

Latex:


\mforall{}[knd:Atom].  \mforall{}[left,right:mFOL()].    (mFOconnect(knd;left;right)  \mmember{}  mFOL())


By

DepprodCoDatatypeConstructorWf  `mFOL\_size`

---

Home Index