The Coq mailing list

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

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