proposition: Lemma lookup_foldr_delete_not_elem_of {A} (m : M A) is j : j ∉ is → foldr delete m is !! j = m !! j.
proof: Proof. induction is; simpl; [done |]. rewrite elem_of_cons; intros. rewrite lookup_delete_ne; intuition. Qed.
imports: Coq(Permutation) stdpp(options)