Commit ec11ab91 authored by Robbert Krebbers's avatar Robbert Krebbers

Stronger saved_prop_agree with equality instead of iff.

parent e86b6558
...@@ -24,12 +24,12 @@ Section saved_prop. ...@@ -24,12 +24,12 @@ Section saved_prop.
Proof. by apply own_alloc. Qed. Proof. by apply own_alloc. Qed.
Lemma saved_prop_agree γ P Q : Lemma saved_prop_agree γ P Q :
(saved_prop_own SPI γ P saved_prop_own SPI γ Q) (P Q). (saved_prop_own SPI γ P saved_prop_own SPI γ Q) (P Q).
Proof. Proof.
rewrite /saved_prop_own -own_op own_valid agree_validI. rewrite /saved_prop_own -own_op own_valid agree_validI.
rewrite agree_equivI later_equivI /=; apply later_mono. rewrite agree_equivI later_equivI /=; apply later_mono.
rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q).
apply (eq_rewrite (iProp_unfold P) (iProp_unfold Q) (λ Q' : iPreProp Λ _, apply (eq_rewrite (iProp_unfold P) (iProp_unfold Q) (λ Q' : iPreProp Λ _,
iProp_fold (iProp_unfold P) iProp_fold Q')%I); solve_ne || auto with I. iProp_fold (iProp_unfold P) iProp_fold Q')%I); solve_ne || auto with I.
Qed. Qed.
End saved_prop. End saved_prop.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment