Tidy PureLang's equational theory

Currently PureLang's equational theory and its results are distributed over various files. We should restructure this carefully:
- `pure_exp_relTheory`: definition of applicative bisimulation and associated theorems
- `pure_howeTheory`: Howe's construction and derivation of congruence
- `pure_congruenceTheory`: general reusable congruence rules

The results in `pure_letrec_congTheory` should be moved to `pure_congruenceTheory`. Other files should be checked for any sufficiently general results and similarly moved.

Start by comparing pure_exp_relTheory, pure_howeTheory, pure_congruenceTheory, and pure_letrec_congTheory to map where the equational results currently live. Move the results from pure_letrec_congTheory into pure_congruenceTheory, identify sufficiently general results in other files, and verify that the reorganized theories retain their intended dependencies and results.

Written by the indexing model from the issue text.