The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

2014-05-06 22:32 GMT+02:00 Jonathan 
<jonikelee AT gmail.com>:
> Goal forall (n : nat), n = S n -> False.
>   intros n H.
>   simplify_eq H.

It does behave like inversion/injection. If you do inversion you also
have a copy of H. This is not a bug, this property needs a real
induction on n to be proved. It is not a consequence of a trivial case
analysis like the one proved by injection/inversion, you need an
induction hypothesis.

Best regards,
Pierre Courtieu