proposition: Lemma lookup_alter_Some {A} (f : A → A) (m : M A) i j y : alter f i m !! j = Some y ↔ (i = j ∧ ∃ x, m !! j = Some x ∧ y = f x) ∨ (i ≠ j ∧ m !! j = Some y).
proof: Proof. destruct (decide (i = j)) as [->|?]. - rewrite lookup_alter. naive_solver (simplify_option_eq; eauto). - rewrite lookup_alter_ne by done. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)