The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 03/07/2013 19:26, t x wrote:
> With apologies for 2 emails in rapid succession -- I realized what I wanted
> in the first case is "replace ... with .... by ... ". However, I'm still
> not sure how to solve the 2nd case (inlining with pose proof ... ).

To do the following:

assert ( _statement_ ) as H0 by _tactic_ .
pose proof (lemma ... H0 ...).

I would use the following trick:

refine
  ((fun (H0 : _statement_) => _ (lemma ... H0 ...)) _); [ |_tactic_].

You can use a tactic notation to do this more neatly, but it should work 
anyway.

PMP