best shot until now of making inductive proofs reduce. Will now change task, but this will probably require changing the high-level Circuit datatype