Add ability to solve unification constraints separately of elaboration of surface syntax

[Russoul]

In extensional type theory we can solve definitional equality constraints via propositional equality, thanks to equality reflection.
That means we can postpone resolution of constraints as far ahead as the end of elaboration of definition/file/module/project!

Moreover, solving those constraints doesn't anyhow change the syntax (nor core nor surface). That's 100% virtual activity, unlike intensional type theory, where solving definitional equality via propositional is only legitimate if we add in transports/coercions along those solutions into the syntax.