kdrag.kernel.einstan

kdrag.kernel.einstan(thm: QuantifierRef) → tuple[list[ExprRef], Proof]

Skolemize an existential quantifier. exists xs, P(xs) -> P(cs) for fresh cs https://en.wikipedia.org/wiki/Existential_instantiation

Parameters:

thm (QuantifierRef)

Return type:

tuple[list[ExprRef], Proof]