Ssreflect Users Discussion List

[Beta Ziliani <>]

Hi ssrs,

Does anybody knows how to generate equations for two parameters using
the [case: _ _/] tactic?

Take for example the following dumb example:

Inductive dummy : nat -> nat -> Prop :=
  | zero : dummy 0 0
  | uno : forall n, dummy n n -> dummy (n.+1) (n.+1).

Goal forall n1 n2 : nat, dummy n1 n2 -> n1 = n2.
move=>n1 n2.
case H: _ _/.

at this point, I have two goals, each of them with an equation
H : n1 = 0
and
H : n1 = _n_.+1
respectively.

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?

Cheers,
Beta