---

Step * of Lemma mRuleorI_wf

∀[left:𝔹]. (mRuleorI(left) ∈ mFOLRule())
BY
{ DepprodCoDatatypeConstructorWf `mFOLRule_size` }

---

Latex:


\mforall{}[left:\mBbbB{}].  (mRuleorI(left)  \mmember{}  mFOLRule())


By

DepprodCoDatatypeConstructorWf  `mFOLRule\_size`

---

Home Index