proposition: Lemma map_agree_delete_l {A} (m1 m2 : M A) i : map_agree m1 m2 → map_agree (delete i m1) m2.
proof: Proof. rewrite !map_agree_alt. intros Hagree j. rewrite lookup_delete_None. destruct (Hagree j) as [|[|<-]]; auto. destruct (decide (i = j)); [naive_solver|]. rewrite lookup_delete_ne; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)