Open
Description
We currently use dependent inductions and destructions with no afterthoughts, leading [JMeq_eq] and [eq_rect_eq] to be pervasive to the whole development.
In the Interaction Trees development, @Lysxia went to great trouble (DeepSpec/InteractionTrees#194) to identify strictly the lemmas requiring those axioms, and showed in the process that a great deal of things can be achieved without them.
We may want to undergo a similar introspection at some point.