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