kdrag.kernel.skolem

kdrag.kernel.skolem(pf: Proof) → tuple[list[ExprRef], Proof]

Skolemize an existential quantifier.

Parameters:: pf (Proof)
Return type:: tuple[list[ExprRef], Proof]