kdrag.kernel.einstan
- kdrag.kernel.einstan(thm: QuantifierRef) tuple[list[ExprRef], None]
Skolemize an existential quantifier. exists xs, P(xs) -> P(cs) for fresh cs https://en.wikipedia.org/wiki/Existential_instantiation
Skolemize an existential quantifier. exists xs, P(xs) -> P(cs) for fresh cs https://en.wikipedia.org/wiki/Existential_instantiation