proposition: Lemma lookup_foldr_delete {A} (m : M A) is j : j ∈ is → foldr delete m is !! j = None.
proof: Proof. induction 1 as [|i j is]; simpl; [by rewrite lookup_delete|]. by destruct (decide (i = j)) as [->|?]; rewrite ?lookup_delete, ?lookup_delete_ne by done. Qed.
imports: Coq(Permutation) stdpp(options)