proposition: Lemma lookup_insert_is_Some {A} (m : M A) i j x : is_Some (<[i:=x]>m !! j) ↔ i = j ∨ i ≠ j ∧ is_Some (m !! j).
proof: Proof. unfold is_Some; setoid_rewrite lookup_insert_Some; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)