Reasoning strategy: rewrite all BDD-building functions into calls of q-ite.
This isn't an especially good reasoning strategy, and we generally prefer equal-by-eval-bdds instead.
canonicalize-to-q-ite is a ruleset that holds theorems for rewriting other BDD-constructing functions into q-ite form.
