Commit 4f0acc79 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Lemma for inclusion of excl similar to dec_agree.

parent 54ede303
...@@ -120,11 +120,11 @@ Lemma excl_validN_inv_l n mx a : ✓{n} (Excl' a ⋅ mx) → mx = None. ...@@ -120,11 +120,11 @@ Lemma excl_validN_inv_l n mx a : ✓{n} (Excl' a ⋅ mx) → mx = None.
Proof. by destruct mx. Qed. Proof. by destruct mx. Qed.
Lemma excl_validN_inv_r n mx a : {n} (mx Excl' a) mx = None. Lemma excl_validN_inv_r n mx a : {n} (mx Excl' a) mx = None.
Proof. by destruct mx. Qed. Proof. by destruct mx. Qed.
Lemma Excl_includedN n a mx : {n} mx Excl' a {n} mx mx {n} Excl' a.
Proof. Lemma Excl_includedN n a b : Excl' a {n} Excl' b a {n} b.
intros Hvalid; split; [|by intros ->]. Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
intros [z ?]; cofe_subst. by rewrite (excl_validN_inv_l n z a). Lemma Excl_included a b : Excl' a Excl' b a b.
Qed. Proof. by intros [[c|] Hb%(inj Some)]; inversion_clear Hb. Qed.
End excl. End excl.
Arguments exclC : clear implicits. Arguments exclC : clear implicits.
......
Supports Markdown
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