kdrag.kernel.forget2

kdrag.kernel.forget2(ts: list[ExprRef], thm: QuantifierRef) → None

“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