---

Step * of Lemma mRuleimpI_wf

impI ∈ mFOLRule()
BY
{ DepprodCoDatatypeConstructorWf `mFOLRule_size` }

---

Latex:


impI  \mmember{}  mFOLRule()


By

DepprodCoDatatypeConstructorWf  `mFOLRule\_size`

---

Home Index