Скажем, у меня есть лемма mylem: foo ?a = bar ?a, и мне нужно применить ее к цели, которая имеет два вхождения foo, например. baz (foo (f p q)) (foo (g r s)), но только в одном из этих положений. Я зн
Если моя цель состояние foo ==> bar --> qux, я знаю, что я могу использовать оператор apply (intro impI)
с получением целевого состояния foo ==> bar ==> qux. Как насчет другого направления? Какая ко