The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Ian Lynagh a écrit :
> In the (very abstracted example of a) lemma below, is there a way to
> prove the result without writing "nat" or "x = y"?
>
> What I'd like is to be able to write something like
> specialize (H _).
>     admit.

There have been several suggestions already, but none that mentioned the
"refine" tactic. So here it comes. "specialize (H _)" can be written

refine (let v := _ in _ (H v)).

Best regards,

Guillaume