Refactor inductive to instead be defined using a subclass of z3's datatype constructor class instead of goofy monkey patched lambdas