Update STYLE, incorporating wiki; close #468

We can't really assert *computation* rules in Coq. These should take the form of (propositional) equalities, presumably. Do we want to say so?