# [isabelle] proving monotonicity

Hi all,
is there any difference in Isabelle\HOL the following two formulas:
1) \<forall>x \<in>A. P(x)
2) \<forall>x. x \<in> A --> P(x)
A is an inductive set.
I would like to use the first solution within a coinductive definition.

`I don't get any error if I use the second solution, but if I use the
``first one the coinductive definition fail to prove the monotonicity .
`
Any advice?
Thanks in advance for the collaboration.
Regards.
-T

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*