kdrag.tactics.subst
- kdrag.tactics.subst(pf: Proof, vs: list[ExprRef], subst: list[ExprRef]) Proof
Perform substitution into a forall quantified proof, instantiating into a new context vs
>>> x,y,z = smt.Reals("x y z") >>> p = kd.prove(smt.ForAll([x,z], smt.And(z == z, x == x))) >>> subst(p, [y, z], [y + 1, z]) |- ForAll([y, z], And(z == z, y + 1 == y + 1))