Step
*
of Lemma
fRuleallI_wf
No Annotations
∀[var:ℤ]. (allI with var ∈ FOLRule())
BY
{ DepprodCoDatatypeConstructorWf' }
Latex:
Latex:
No  Annotations
\mforall{}[var:\mBbbZ{}].  (allI  with  var  \mmember{}  FOLRule())
By
Latex:
DepprodCoDatatypeConstructorWf'
Home
Index