Step
*
of Lemma
FormAnd_wf
∀[C:Type]. ∀[left,right:Form(C)].  (left ∧ right) ∈ Form(C))
BY
{ DepprodCoDatatypeConstructorWf `Form_size` }
Latex:
Latex:
\mforall{}[C:Type].  \mforall{}[left,right:Form(C)].    (left  \mwedge{}  right)  \mmember{}  Form(C))
By
Latex:
DepprodCoDatatypeConstructorWf  `Form\_size`
Home
Index