kdrag.tactics.ForAllI

kdrag.tactics.ForAllI(vs: list[ExprRef], pf: Proof) → Proof

All vs must be FreshVars Combinator name tries to make it clear that this is a smt.ForAll that works on Proofs instead of BoolRefs.

Parameters:

• vs (list[ExprRef])

• pf (Proof)

Return type:

Proof