 <p>What you want to do is not called "instantiation." You can instantiate a universally quantified hypothesis and you can instantiate an existentially quantified conclusion, but not vice versa. I'm thinking the proper name is "introduction". You can introduce existential quantification in a hypothesis and you can introduce universal quantification in the conclusion. If it seems like you're "eliminating" instead, that's because, when proving something, you start at the bottom of a sequent calculus deriviation, and work your way backwards to the top.</p> <p>Anyway, use the tactic <code>firstorder</code>. Also, use the command <code>Set Firstorder Depth 0</code> to turn off proof search if you only want to simplify your goal.</p> <p>If your goal has higher order elements though, you'll probably get an error message. In that case, you can use something like <code>simplify</code>.</p> <pre><code>Ltac simplify := repeat match goal with | h1 : False |- _ =&gt; destruct h1 | |- True =&gt; constructor | h1 : True |- _ =&gt; clear h1 | |- ~ _ =&gt; intro | h1 : ~ ?p1, h2 : ?p1 |- _ =&gt; destruct (h1 h2) | h1 : _ \/ _ |- _ =&gt; destruct h1 | |- _ /\ _ =&gt; constructor | h1 : _ /\ _ |- _ =&gt; destruct h1 | h1 : exists _, _ |- _ =&gt; destruct h1 | |- forall _, _ =&gt; intro | _ : ?x1 = ?x2 |- _ =&gt; subst x2 || subst x1 end. </code></pre>