The Coq mailing list

[Edsko de Vries <Edsko.de.Vries AT cs.tcd.ie>]

Never mind, it's not true...

On Sat, Mar 21, 2009 at 09:20:28AM +0000, Edsko de Vries wrote:
> Hi,
> 
> I am stuck in a proof with lots of JMeqs. I've tried to make a minimal 
> example
> that shows the problem; hopefully it's not too minimal. The question is 
> simple:
> how can I complete the following proof??
> 
> Require Import JMeq.
> 
> Section test.
> 
> Variables A B : Set.
> Variables (a : A) (b : B).
> 
> Hypothesis a_equals_b : JMeq a b.
> 
> Definition t (cond : bool) : Set :=
>   match cond with
>   | true => A -> A
>   | false => B -> B
>   end.
> 
> Variable f : forall (cond : bool), t cond.
> 
> Lemma foo :
>   JMeq (f true a) (f false b).
> Proof.
> 
> Any help is greatly appreciated!
> 
> Edsko
> 
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club