Ssreflect Users Discussion List

[Cyril Cohen <>]

Dear Beta,

Le 28/01/2014 19:27, Beta Ziliani a écrit :
> What I'm interested in is in having also an equation for n2. According
> to the manual this is not possible, but is there a way of achieving
> this without having to fall back to inversion?

Is this close to what you want?

Goal forall n1 n2 : nat, dummy n1 n2 -> n1 = n2.
move=> n1 n2 dummyn.
case: {-2}_ {-2}_ / dummyn (erefl n1) (erefl n2).

Cheers,
-- 
Cyril