Commit a4dc90a9 authored by Ralf Jung's avatar Ralf Jung
Browse files

add lookup_union_l

parent ddce76d7
Pipeline #49681 passed with stage
in 5 minutes and 32 seconds
......@@ -1988,6 +1988,9 @@ Proof. apply lookup_union_with. Qed.
Lemma lookup_union_r {A} (m1 m2 : M A) i :
m1 !! i = None (m1 m2) !! i = m2 !! i.
Proof. intros Hi. by rewrite lookup_union, Hi, (left_id_L _ _). Qed.
Lemma lookup_union_l {A} (m1 m2 : M A) i :
is_Some (m1 !! i) (m1 m2) !! i = m1 !! i.
Proof. intros [x Hi]. rewrite lookup_union, Hi. by destruct (m2 !! i). Qed.
Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x :
(m1 m2) !! i = Some x
m1 !! i = Some x (m1 !! i = None m2 !! i = Some x).
......
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