Improvements to make_equiv

[jdchristensen]

The first commit changes cbn to hnf in the make_equiv tactic, so that the lazymatch can correctly detect path types. If the path type was hidden in record or class, like IsUnitPreserving, then make_equiv would inadvertently destruct it with elim. With the change, one proof in Group.v becomes much simpler. make_equiv failed there before this change.

The second commit is independent and just gives some improvements coming from looking at places where make_equiv was used. The cbn inserted in one spot speeds up the make_equiv there.

[jdchristensen]

I tested that the change to hnf has no measurable affect on the build time.

[Alizter]

Fantastic!