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