---

Step * of Lemma mRuleexistsI_wf

∀[var:ℤ]. (existsI with var ∈ mFOLRule())
BY
{ DepprodCoDatatypeConstructorWf `mFOLRule_size` }

---

Latex:


\mforall{}[var:\mBbbZ{}].  (existsI  with  var  \mmember{}  mFOLRule())


By

DepprodCoDatatypeConstructorWf  `mFOLRule\_size`

---

Home Index