proposition: Lemma map_agree_foldr_delete_r {A} (m1 m2 : M A) is : map_agree m1 m2 → map_agree m1 (foldr delete m2 is).
proof: Proof. induction is; simpl; auto using map_agree_delete_r. Qed.
imports: Coq(Permutation) stdpp(options)