Turn `internal_eq_entails` into a bi-implication

I don't think the other direction is derivable, but I would like to be proved wrong.

The other direction is particularly useful if you want to turn an "internal" proof (i.e., in the Iris logic, without exposing step-indexing) of non-expansiveness/contractiveness into an "external" proof of a Proper/Contractive instance.