Ensure that different `Cofe` proofs of `iProp` are convertible.

Cofe proofs often occur at relevant positions, e.g., as an argument of fixpoint. This MR makes sure that if difference Cofe proofs for iProp are picked, they are convertible.