---

Step * of Lemma mRuleandE_wf

∀[hypnum:ℕ]. (andE on hypnum ∈ mFOLRule())
BY
{ DepprodCoDatatypeConstructorWf `mFOLRule_size` }

---

Latex:


\mforall{}[hypnum:\mBbbN{}].  (andE  on  hypnum  \mmember{}  mFOLRule())


By

DepprodCoDatatypeConstructorWf  `mFOLRule\_size`

---

Home Index