proposition: Lemma foldr_delete_notin {A} (m : M A) is : Forall (λ i, m !! i = None) is → foldr delete m is = m.
proof: Proof. induction 1; simpl; [done |]. rewrite delete_notin; congruence. Qed.
imports: Coq(Permutation) stdpp(options)