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 (https://github.com/DeepSpec/InteractionTrees/pull/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.
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 (https://github.com/DeepSpec/InteractionTrees/pull/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.