Changed primitives over to expressions to make proofs easier.