kdrag.kernel.forget

kdrag.kernel.forget(ts: Sequence[ExprRef], thm: QuantifierRef) → Proof

“Forget” a term using existentials. This is existential introduction. P(ts) -> exists xs, P(xs) thm is an existential formula, and ts are terms to substitute those variables with. forget easily follows. https://en.wikipedia.org/wiki/Existential_generalization

Parameters: