Ssreflect Users Discussion List

[Beta Ziliani <>]

Hi list,

I have a (probably stupid) question regarding ssr tactics.  Say that I
have the following simple goal:

(P -> Q) -> R

and I'd like to get Q with a proof of P.  If I have a proof of P,
say x, this is simple:

move/(_ x).

Now, if I don't have the proof of P beforehand, I'd like to do something like

move/(_ _).

and have P as a subgoal.  This doesn't work (more precisely, it does
nothing).  Is there a simple way of getting a subgoal P and a goal Q
-> R?  I want to avoid having to write what P is, of course, otherwise
it'd be easy.

Thanks in advance,
Beta