---

Step * of Lemma mRuleallE_wf

No Annotations
∀[hypnum:ℕ]. ∀[var:ℤ].  (allE on hypnum with var ∈ mFOLRule())
BY
{ DepprodCoDatatypeConstructorWf' }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[hypnum:\mBbbN{}].  \mforall{}[var:\mBbbZ{}].    (allE  on  hypnum  with  var  \mmember{}  mFOLRule())


By

---

Latex:
DepprodCoDatatypeConstructorWf'

---

Home Index