title: How to instantiate a variable of forall in a hypothesis in Coq?
body: <p>I have two hypotheses</p>
  
  <pre><code>IHl: forall (lr : list nat) (d x : nat), d = x \/ In x l' -&gt; (something else)
  Head : d = x
  </code></pre>
  
  <p>I want to <code>apply IHl</code> on <code>Head</code> as it satisfies <code>d = x \/ In x l</code> of IHl. I tried <code>apply with</code> tactic which fails with a simple hint <code>Error: Unable to unify</code>.</p>
  
  <p>Which tactic should I use to instantiate variables in a hypothesis?</p>