Clean up dataLang cost semantics

This issue is to clean up some of the mess we made when introducing the dataLang cost semantics.

- The `allowed_op` definition serves no purpose anymore --- all operators except Install are now allowed, and Install is already treated specially elsewhere in `do_app`
- Much (all?) of `costProps` should move from `examples/cost` into `dataProps` (because part of it is needed in `data_to_word_assignProof` and hence copypasted)
- The `wordLang` stack cost semantics would be much nicer if it was phrased in the `option_le` style of the `dataLang` layer instead of the `the F ...` "style" it currently uses.
- dataProps has many slow and eerily similar `do_app` proofs. Can these be sped up or fused together?