Dead code + typo.
Basic lemmas about the algebraic structure of equality.
Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").
Fixing introduction patterns * and ** when used in a branch so that they do not introduce beyond what is under control of the branch. See test-suite intros.v for an example.
More on injection over a projectable "existT". - Fixing syntax "injection ... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities).