The Coq mailing list

[richard dapoigny <richard.dapoigny AT univ-savoie.fr>]

Le 27/04/2015 15:57, Pierre Courtieu a écrit :
> Hi,
>
> This is no true and therefore not provable.
>
> But if you add parenthesis over the first quantified part then it is a
> different property (and probably the on one you meant?) that is
> provable by "intro h; assumption."
>
> (forall x, (* some complex function depending on x*)) -> forall y, (*
> the same complex function depending on y*)
>
> For examepl:
>
> Variable A:Type.
> Variable P: Type -> Prop.
>
> Goal (forall x, (P x)) -> (forall y, P y).
> Proof.
>    intro h.
>    assumption.
>
> Best regards,
> Pierre
Thanks for the prompt answer!
Yes I would like to have the goal you suggest but the problem is that 
the left part is generated by applying generalize x Hi (wher Hi is 
another hypothesis) and therefore I cannot obtain the whole expression 
due to a lack of parentheses
> 2015-04-27 15:42 GMT+02:00 richard dapoigny 
> <richard.dapoigny AT univ-savoie.fr>:
> > Hi all,
> > I try to demonstrate a goal having the form:
> > forall x, (* some complex function depending on x*) -> forall y, (* the same
> > complex function depending on y*)
> > Is there a simple way to do it?
> > Thanks in advance,
> > Richard