applyS t auto_params


applyS sterm auto_params


t must have type T1 → ... → Tn → G.


applyS is useful when apply fails because the current goal and the conclusion of the applied theorems are extensionally equivalent up to instantiation of metavariables, but cannot be unified. E.g. the goal is P(n*O+m) and the theorem to be applied proves ∀m.P(m+O).

It tries to automatically rewrite the current goal using auto paramodulation to make it unifiable with G. Then it closes the current sequent by applying t to n implicit arguments (that become new sequents). The auto_params parameters are passed directly to auto paramodulation.

New sequents to prove:

It opens a new sequent for each premise Ti that is not instantiated by unification. Ti is the conclusion of the i-th new sequent to prove.