Remove "old" values

Infinite coinductive values are defined in `pure_valueTheory`, but no longer necessary. However, they can't be removed easily because some value-based results are lifted to weak-head results (e.g. using `eval_eq_imp_app_similarity`). The corresponding results for weak-head forms should be derived, and the old coinductive values deleted. This should permit removal of several files (`pure_valueTheory`, `quotient_llistTheory`, `pure_limitTheory`), and various other definitions/lemmas. It would also require deletion of `pure_eval_surjTheory`.

Start by tracing the value-based results that use eval_eq_imp_app_similarity and identify the corresponding weak-head results that must be derived. Review pure_valueTheory, quotient_llistTheory, pure_limitTheory, and pure_eval_surjTheory along with their dependencies. Done means the weak-head results replace the old lifts and the obsolete files, definitions, and lemmas can be removed without breaking the theory.

Written by the indexing model from the issue text.