Trick suggestion #18
Description
I found the exploit tactic useful in case where I have H : P -> Q in the context or as a lemma and would like to have Q in the context with the assumption P left as a subgoal. The tactic is defined in: https://github.com/AbsInt/CompCert/blob/27beb944ff6ff18ea612c116e414eb40ce1320a6/lib/Coqlib.v#L57