Skip to content

Soundness lemma for internal equality of `uPred`.

Robbert Krebbers requested to merge robbert/internal_eq_soundness into master

This MR adds the result:

Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True  x  y)  x  y.

Merge request reports