proposition: Lemma lookup_insert_None {A} (m : M A) i j x : <[i:=x]>m !! j = None ↔ m !! j = None ∧ i ≠ j.
proof: Proof. split; [|by intros [??]; rewrite lookup_insert_ne]. destruct (decide (i = j)) as [->|]; rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence. Qed.
imports: Coq(Permutation) stdpp(options)