Step
*
of Lemma
mRuleimpE_wf
∀[hypnum:ℕ]. (impE on hypnum ∈ mFOLRule())
BY
{ DepprodCoDatatypeConstructorWf `mFOLRule_size` }
Latex:
\mforall{}[hypnum:\mBbbN{}].  (impE  on  hypnum  \mmember{}  mFOLRule())
By
DepprodCoDatatypeConstructorWf  `mFOLRule\_size`
Home
Index