It would be better if coqutil used no axioms

[JasonGross]

coqchk gives:

CONTEXT SUMMARY
===============

* Theory: Set is predicative

* Axioms:
    Coq.ssr.ssrunder.Under_rel.Over_rel
    Coq.ssr.ssrunder.Under_rel.Under_rel_from_rel
    Coq.ssr.ssrunder.Under_rel.over_rel
    Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
    coqutil.Map.SortedList.TODO_andres
    Coq.ssr.ssrunder.Under_rel.over_rel_done
    Coq.ssr.ssrunder.Under_rel.Under_rel
    Coq.Logic.PropExtensionality.propositional_extensionality
    Coq.ssr.ssrunder.Under_rel.Under_relE
    coqutil.Map.SortedListString.TODO_andres
    Coq.ssr.ssrunder.Under_rel.under_rel_done

* Constants/Inductives relying on type-in-type: <none>

* Constants/Inductives relying on unsafe (co)fixpoints: <none>

* Inductives whose positivity is assumed: <none>

You can ignore the ssr.ssrunder ones (coq/coq#5030), but it'd be nice to remove the other ones.

[samuelgruetter]

The TODOs in coqutil.Map are scheduled to be fixed soon, but we weren't planning to remove functional and prop extensionality

[JasonGross]

What's the reason you use Leibniz equality on sets rather than defining your own equivalence relation on them? As far as I can tell, doing this would allow you to remove all your uses of propext and most of your uses of funext.

[mdempsky]

I sent PR #26 to remove coqutil.Map.SortedList.TODO_andres.

[andres-erbsen]

Merged, thanks!

[andres-erbsen]

Trickling down at mit-plv/bedrock2#153 ...