Reintroduce Term Size Optimizations

[hargoniX]

sat_decide used to have an optimization such that it would only generate a proof term during reflection if the terms where not already defeq. This can enable a drastic reuse of proof term size and thus faster type checking on enormous proof goals.

We should add this to bv_decide of goal size becomes an issue again.