The Coq mailing list

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

Taral a écrit :

> I need this somehow:
>
> Variable var : Type.
>
> Inductive test : Type :=
> | A : var -> test
> | B : test.
>
> Goal forall T (f : T -> test) x y v, f x = A v -> exists v', f y = A v'.
>
> Any ideas? Impossible?
>
>  
It looks wrong when applied to
var := nat,
T := nat,
f (n):= if n=0 then B else A(n),
x :=v := 1,
y :=0 ,
in which case you could prove the contrary.

ah