Commit 6923de66 authored by Robbert Krebbers's avatar Robbert Krebbers

Make auth_frag_op a Leibniz equality.

parent 42cf780a
...@@ -193,7 +193,7 @@ Lemma auth_validI {M} (x : auth A) : ...@@ -193,7 +193,7 @@ Lemma auth_validI {M} (x : auth A) :
end : uPred M). end : uPred M).
Proof. uPred.unseal. by destruct x as [[[]|]]. Qed. Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
Lemma auth_frag_op a b : (a b) a b. Lemma auth_frag_op a b : (a b) = a b.
Proof. done. Qed. Proof. done. Qed.
Lemma auth_frag_mono a b : a b a b. Lemma auth_frag_mono a b : a b a b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed. Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
......
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