Рассуждения с сопоставлениями с образцами в Coq

Question

Если у меня есть гипотеза вида

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

Как я могу вывести G = C x? Спасибо!

Answer 1

Пожалуйста, отправьте полные примеры; скорее всего, в вашем случае destruct G; congruence должен добиться цели.