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