Catch incorrect operations for types

[wwitzel]

trafficstars

For example, it is easy to use Add, Mult, Sum, etc instead of VecAdd, ScalarMult, VecSum, etc. These are intentionally different types of Expressions because functionality needs to be different, though it isn't otherwise necessary for their operations to be distinct (there should be no inherent contradictions through extended meanings. One downside to Prove-It not requiring types to be specified up front is that it can be hard to catch such mistakes early. But it should be possible to catch these mistakes early enough with a bit of cleverness. It is something to think through.