Added IntoPure instance to simplify internal bi equalities into a pure leibniz equality.

For !930, we want to automatically simplify the introduction of a ≡ b : PROP into the pure fact a = b : Prop whenever possible.
This avoids users having to do something like H%leibniz_equiv.

This MR accomplishes that by adding a second IntoPure instance for a ≡ b : PROP, which also makes the simplification happen when using iIntros, on goals like ⊢ a ≡ b -∗ P.

One question I did have: the LeibnizEquiv typeclass currently has Hint Mode ! -, signifying that the type is an input, while the equivalence which is supposed to imply leibniz equality is an output. Should that be Hint Mode ! !, i.e., both are inputs?