title: Coq tactic that adds the value of an inductive term to the context
body: <p>Just to give a simple example of this issue I keep running into, suppose I wish to prove <code>forall f : nat -&gt; bool, exists i j, i&lt;&gt;j /\ f i = f j.</code>  The obvious thing to do is check the values of <code>f 0, f 1, f 2,</code> and proceed accordingly.  However, if I simply say <code>destruct (f 0)</code>, Coq doesn't modify the goal, since <code>f 0</code> doesn't occur as a subterm.  Therefore, I don't have the information I want about what value <code>f 0</code> is currently taking.  Ideally, I would like for Coq to add a witness <code>H : f 0 = false</code> to the context so I can keep track of it.</p>
  
  <p>What I've been doing to get around these issues is to prove an auxiliary lemma <code>bool_destruct : forall b : bool, b = false \/ b = true</code>.  Now, if I say <code>destruct (bool_destruct (f 0))</code> Coq will add the desired <code>H</code> to the context.  Naturally, this is tedious when you have to prove this sort of lemma for each inductive type.  Thus, I'm wondering if there is a nice tactic that handles these sorts of situations. </p>