Skip to content

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

Robbert Krebbers requested to merge robbert/bi_cofe into master

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.

Merge request reports