Preconditions in compiler translation

Currently, translating the PureCake compiler produces many preconditions. Some of these are due to the translator itself (e.g. requiring more congruence rules). But some could potentially be avoided on the PureCake side, or discharged via manual proof. This issue is about going through these to figure out exactly what needs to be done, and doing as much of it as possible from the PureCake side.