Предположим, у меня есть гипотеза H : forall ( x : X ), P x и переменная x : X в контексте. Я хочу выполнить универсальное инстанцирование и получить новую гипотезу H' : P x. Как это сделать наиболее безболезненно? Видимо apply H in x не работает. assert ( P x ), за которым следует apply H, делает, но это может стать очень запутанным, если P сложное.
Есть похожий вопрос, который кажется несколько связанным. Хотя не уверен, что его можно здесь применить.
