Q:

Proof by cases on a boolean expression in Coq

I have a contains function:
Fixpoint contains (l: list string) (x: string): bool :=
  match l with
  | [] => false
  | h :: tl => (if (string_dec h x) then true else (contains tl x))
  end. 

which checks if a string is in a list of strings.  I would like to prove a theorem by doing case analysis on whether contains (vars e) y holds.  However, when I destruct on this boolean I don't get any extra hypothesis for the different subcases.  
How can I solve this issue? 

A:

If you want to get the corresponding assumptions, use "eqn" to give a name for them.  that is: 
destruct (contains (vars e) y) eqn:name.