logic - apply を使用して Coq で含意を「抽出」する方法

Question

例を使って説明します。

H : R -> P -> Q

H0 : R

サブゴール:

(Q -> P) \ / (P -> Q)

私の質問は、どのように抽出するかです (P->Q)。私はすでに R を持っていますが、「H0 に H を適用」すると、すべてが評価され、Q が返されます。