Coq中的模式匹配推理

Question

如果我有一个形式的假设

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

如何推断G = C x？谢谢！

Answer 1

请提交完整的示例;可能就您而言destruct G; congruence应该可以解决问题。