Make box a definition and prove it contractive

This also allows us to get rid of ctx_eq.

However, I have the feeling that some things got significantly slower; CI will tell us. Also, some of the automation does not work any more, as can be seen by my changes in the respective type-checking proofs. @jjourdan could you help me with that? I don't even understand why these things used to work, or what changed about them now...

Unfortunately this exactly confirms what I dislike about these eauto-based proofs... if they fail, it is pretty much impossible to debug what is going on unless you are the person that carefully designed these hint dbs in the first place. For example, it took me more than 30 minutes to even realize that there is a second hint db lrust_typing_merge. Until then I had used Print HintDb lrust_typing, and then focused only on the lemmas that came up there. @jjourdan any chance you could document which pieces are working together how, and which priorities have been carefully tuned? And by "document" I mean "written down in some file in the project root"; not "half a dozen comments spread across the entire development". Right now, solve_typing is to a large extend a mystery to me (at least to the extend that it is broken after I introduced box as a definition).