The Coq mailing list

[Taral <taralx AT gmail.com>]

On Tue, Nov 18, 2008 at 3:19 PM, André Hirschowitz 
<ah AT unice.fr>
 wrote:
> 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.

The point is that f is parametric in var. Try this instead:

Inductive test (var : Type) : Type :=
| A : var -> test var
| B : test var.

Goal forall T var (f : forall var, T -> test var) x y v, f var x = A
var v -> exists v', f var y = A var v'.

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown