Supongamos que tengo una hipótesisH : forall ( x : X ), P x y una variablex : X en el contexto. Quiero realizar una instanciación universal y obtener una nueva hipótesisH' : P x. ¿Cuál es la forma más indolora de hacer esto? Aparentementeapply H in x No funciona.assert ( P x ) seguido porapply H lo hace, pero puede ser muy complicado siP es complejo.

Hay unapregunta similar eso parece algo relacionado. Sin embargo, no estoy seguro de si se puede aplicar aquí.