The Coq mailing list

["JAEGER, Eric (SGDN)" <eric.jaeger AT sgdn.gouv.fr>]

> 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'.

Sorry, but I do not understand either. Nothing prevents f to return B for 
some y, even once you have exhibited a value x such that f x=A v. In such a 
case your goal appears false.

By the way, f var x=A v proves that var is not empty only if you assume that 
T is not (but I agree that if T is empty then your goal is trivially true).

   Regards, Eric