The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

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


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