[feature request] Support operation with assuming function extensionality

[RalfJung]

Right now, function extensionality as pulled in by asimpl is the only axiom we use in our entire Coq development.

Considering that this is ultimately about proving equality of source terms, which have decidable equality, function extensionality should not be necessary here. It would be nice if the axiom could be avoided :)

[tebbi]

Thank you for the suggestion!

I am currently re-designing Autosubst from scratch, so it does not make much sense to implement this feature in a soon to be dead branch. Apart from that, yes, I plan to do this, but since it complicates matters, only once I am fully convinced of the design.