applyS sterm auto_params

t must have type T₁ → ... → T_n → 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.

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