Я пытаюсь научиться делать автоматизацию Coq proof à la Chlipala / crush.В связи с этим мне интересно, каков удобный подход для автоматического разбиения индуктивных типов по одному случаю, например, при решении следующих задач:
Goal forall {A B: Prop}, (A <-> B) -> (A -> B).
Goal forall {A B: Type}, A * B -> A.
Я бы хотел автоматически разбивать их только тогда, когдаимеет смысл - то есть, только когда я не теряю при этом никакой информации.Это возможно?