Rework evaluation semantics to not be arguing about precondition, make this explicit in the theorem, that we assume it. Admitted proofs that are obvious