Step 
*
 of Lemma 
intformand_wf
∀[left,right:int_formula()].  (left "∧" right ∈ int_formula())
BY
 
{ DepprodCoDatatypeConstructorWf `int_formula_size` }
 
Latex: 
Latex:
\mforall{}[left,right:int\_formula()].    (left  "\mwedge{}"  right  \mmember{}  int\_formula())
 By 
Latex:
DepprodCoDatatypeConstructorWf  `int\_formula\_size`
Home
Index