proposition: Lemma lookup_foldr_delete_Some {A} (m : M A) is j y : foldr delete m is !! j = Some y ↔ j ∉ is ∧ m !! j = Some y.
proof: Proof. induction is; simpl; rewrite ?lookup_delete_Some; set_solver. Qed.
imports: Coq(Permutation) stdpp(options)