# 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?

Edited by Ike Mulder