proposition: Lemma lookup_delete_is_Some {A} (m : M A) i j : is_Some (delete i m !! j) ↔ i ≠ j ∧ is_Some (m !! j).
proof: Proof. unfold is_Some; setoid_rewrite lookup_delete_Some; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)