proposition: Lemma lookup_insert_is_Some' {A} (m : M A) i j x : is_Some (<[i:=x]>m !! j) ↔ i = j ∨ is_Some (m !! j).
proof: Proof. rewrite lookup_insert_is_Some. destruct (decide (i=j)); naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)