coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] forall implication

From: richard dapoigny <richard.dapoigny AT univ-savoie.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] forall implication
Date: Mon, 27 Apr 2015 15:42:30 +0200
Organization: LISTIC

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

[Coq-Club] Last Call: The Coq workshop, deadline April 30th, 2015, bertot, 04/21/2015
- [Coq-Club] forall implication, richard dapoigny, 04/27/2015
  - Re: [Coq-Club] forall implication, Pierre Courtieu, 04/27/2015
    - Re: [Coq-Club] forall implication, richard dapoigny, 04/27/2015
      - Re: [Coq-Club] forall implication, Pierre Courtieu, 04/27/2015
        
        Re: [Coq-Club] forall implication, richard dapoigny, 04/27/2015
        
        RE: [Coq-Club] forall implication, Soegtrop, Michael, 04/27/2015
        
        Re: [Coq-Club] forall implication, Richard Dapoigny, 04/27/2015