Ssreflect Users Discussion List

[Cyril Cohen <>]

Le 28/01/2014 19:59, Cyril Cohen a écrit :
> case: {-2}_ {-2}_ / dummyn (erefl n1) (erefl n2).

With {-1} instead (I had Coq, I should have tested).

but Enrico's solution works as well:

Goal forall n1 n2 : nat, dummy n1 n2 -> n1 = n2.
move=> n1 n2 dummyn.
case H1: _ {-1}_ / dummyn (erefl n2) => [|n dummyn].

and of course if you use this induction principle regularly, you might want to
do a specific _spec inductive as Enrico said :).

Cheers,
-- 
Cyril