kdrag.kernel.instan

kdrag.kernel.instan(ts: Sequence[ExprRef], pf: Proof) → Proof

Instantiate a universally quantified formula. This is forall elimination

Parameters:

• ts (Sequence[ExprRef])

• pf (Proof)

Return type:

Proof