The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Ok thank you all.
>    inversion 1; reflexivity.
This is not working in the "real" setting, so I tried to understand
the first proposal,
That IS actually working for my real needs.
However I doesn't understand the coq behaviour here: that is:

if I make
unfold rK;intros n myR.
 generalize (refl_equal (f n)).

I obtain

forall e : f n = f n,
Some myR =
(if f n as x return (x = f n -> option R)
 then fun p : true = f n => Some (r n p)
 else fun _ : false = f n => None) e -> data myR = n

that is quite unexpected. I was expecting

f n = f n ->
Some myR =
(if f n as x return (x = f n -> option R)
 then fun p : true = f n => Some (r n p)
 else fun _ : false = f n => None) (refl_equal (f n)) -> data myR = n

(that is exactly what I obtain doing
intros n myR.
 generalize (refl_equal (f n)).
unfold rK.)

It looks like generalize is much more complex that I expected. When
this forall e is generated??