Clean up dataLang cost semantics

[IlmariReissumies]

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?