title: How to eliminate a disjunction inside of an expression?
body: <pre><code>Lemma In_map_iff :
    forall (A B : Type) (f : A -&gt; B) (l : list A) (y : B),
      In y (map f l) &lt;-&gt;
      exists x, f x = y /\ In x l.
  Proof.
  split.
  - generalize dependent y.
    generalize dependent f.
    induction l.
    + intros. inversion H.
    + intros.
      simpl.
      simpl in H.
      destruct H.
      * exists x.
        split.
        apply H.
        left. reflexivity.
      * 
  </code></pre>
  
  <hr>
  
  <pre><code>1 subgoal
  A : Type
  B : Type
  x : A
  l : list A
  IHl : forall (f : A -&gt; B) (y : B),
        In y (map f l) -&gt; exists x : A, f x = y /\ In x l
  f : A -&gt; B
  y : B
  H : In y (map f l)
  ______________________________________(1/1)
  exists x0 : A, f x0 = y /\ (x = x0 \/ In x0 l)
  </code></pre>
  
  <p>Since proving <code>exists x0 : A, f x0 = y /\ (x = x0 \/ In x0 l)</code> is the same as proving <code>exists x0 : A, f x0 = y /\ In x0 l</code>, I want to eliminate <code>x = x0</code> inside the goal here so I can apply the inductive hypothesis, but I am not sure how to do this. I've tried <code>left in (x = x0 \/ In x0 l)</code> and various other things, but I haven't been successful in making it happen. As it turns out, defining a helper function of type <code>forall a b c, (a /\ c) -&gt; a /\ (b \/ c)</code> to do the rewriting does not work for terms under an existential either.</p>
  
  <p>How could this be done? </p>
  
  <p>Note that the above is one of the SF book exercises.</p>