Step
*
of Lemma
mRuleexistsE_wf
∀[hypnum:ℕ]. ∀[var:ℤ].  (existsE on hypnum with var ∈ mFOLRule())
BY
{ DepprodCoDatatypeConstructorWf `mFOLRule_size` }
Latex:
\mforall{}[hypnum:\mBbbN{}].  \mforall{}[var:\mBbbZ{}].    (existsE  on  hypnum  with  var  \mmember{}  mFOLRule())
By
DepprodCoDatatypeConstructorWf  `mFOLRule\_size`
Home
Index