The Coq mailing list

[Andr� Hirschowitz <ah AT unice.fr>]

Hello,

My first impression is that you cannot:
Take 
A:=B = bool.
a=b=true
and
f (true) =Id, f(false) = -Id
Probably you oversimplified your problem?

ah
> 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
>