A version of `to_agree_uninj` in the logic.

e6d61427 · Robbert Krebbers · 7b0f3340 · e6d61427
Commit e6d61427 authored Dec 10, 2018 by Robbert Krebbers
Show whitespace changes
Inline Side-by-side

Showing with 3 additions and 0 deletions

theories/algebra/agree.v theories/algebra/agree.v +3 -0

No files found.
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -241,6 +241,9 @@ Proof.
 Qed.
 Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢@{uPredI M} x ≡ y.
 Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
+
+Lemma to_agree_uninjI {M} x : ✓ x ⊢@{uPredI M} ∃ a, to_agree a ≡ x.
+Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
 End agree.

 Instance: Params (@to_agree) 1.