Fix test-suite script for HoTT coq bug #34
The test-suite file couldn't typecheck as it rightly introduces a universe inconsistency.
One needs to use a universe level lower than eq's parameter for this to be consistent.
The uses of the funext axiom forced levels to Set, relaxing its use doesn't.
Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.
Fix semantics of change p with c to typecheck c at each specific occurrence of p,
avoiding unwanted universe constraints in presence of universe polymorphic constants.
Fixing HoTT bugs # 36, 54 and 113.