Reasoning with pattern matchings in Coq

Question

If I have a hypothesis of the form

H: match G with
   | C x => e
   | _ => None
   end = Some T

How can I deduce G = C x ? Thanks!

Answer 1

Please submit complete examples; likely in your case destruct G; congruence should do the trick.