Step 
*
 of Lemma 
mRuleimpI?_wf
∀[v:mFOLRule()]. (mRuleimpI?(v) ∈ 𝔹)
BY
 
{ DepprodCoDatatypeRecognizerWf }
 
Latex: 
Latex:
\mforall{}[v:mFOLRule()].  (mRuleimpI?(v)  \mmember{}  \mBbbB{})
 By 
Latex:
DepprodCoDatatypeRecognizerWf
Home
Index