Angenommen, ich habe eine HypotheseH : forall ( x : X ), P x und eine Variablex : X im Kontext. Ich möchte eine universelle Instanziierung durchführen und eine neue Hypothese erhaltenH' : P x. Was ist der schmerzloseste Weg, dies zu tun? Anscheinendapply H in x funktioniert nicht.assert ( P x ) gefolgt vonapply H tut, aber es kann sehr chaotisch werden, wennP ist komplex.

Da ist ein ähnliche Frage das scheint etwas verwandt zu sein. Ich bin mir nicht sicher, ob es hier angewendet werden kann.