fin_maps.v 486 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
From stdpp Require Import fin_maps.

Section map_disjoint.
  Context `{FinMap K M}.

  Lemma solve_map_disjoint_singleton_1 {A} (m1 m2 : M A) i x :
    m1 ## <[i:=x]> m2  {[ i:= x ]}  m2 ## m1  m2 ## .
  Proof. intros. solve_map_disjoint. Qed.

  Lemma solve_map_disjoint_singleton_2 {A} (m1 m2 : M A) i x :
    m2 !! i = None  m1 ## {[ i := x ]}  m2  m2 ## <[i:=x]> m1  m1 !! i = None.
  Proof. intros. solve_map_disjoint. Qed.
End map_disjoint.