Step
*
of Lemma
mRuleimpI_wf
impI ∈ mFOLRule()
BY
{ DepprodCoDatatypeConstructorWf `mFOLRule_size` }
Latex:
impI  \mmember{}  mFOLRule()
By
DepprodCoDatatypeConstructorWf  `mFOLRule\_size`
Home
Index