Skip to content
GitLab

Soundness lemma for internal equality of `uPred`.

Merged 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.