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