kdrag.rewrite.rule_of_theorem

kdrag.rewrite.rule_of_theorem(thm: BoolRef | QuantifierRef) → RewriteRule

Unpack theorem of form forall vs, lhs = rhs into a Rule tuple

>>> x = smt.Real("x")
>>> rule_of_theorem(smt.ForAll([x], x**2 == x*x))
RewriteRule(vs=[X...], lhs=X...**2, rhs=X...*X...)