Suponha que eu tenha uma hipóteseH : forall ( x : X ), P x e uma variávelx : X no contexto. Quero executar instanciação universal e obter uma nova hipóteseH' : P x. Qual é a maneira mais indolor de fazer isso? Pelo vistoapply H in x não funciona.assert ( P x ) Seguido porapply H mas pode ficar muito confuso seP é complexo.

Há umpergunta semelhante isso parece um pouco relacionado. Não tenho certeza se pode ser aplicado aqui, no entanto.