Make HoTT compile with latest trunk.

Mainly Set Keyed Unification directives + one explicit rewrite due to the fact that rewrite has
changed in the trunk and is not able to use previous instances of holes to unify later terms
(move from metas to evars). I'm not sure how this compares in terms of time but I'd like HoTT/HoTT to sync with coq's trunk again especially because we'll be branching to 8.5 soon and it would be good to have a HoTT that works with the upcoming beta, ideally the current version.