proposition: Lemma lookup_partial_alter_Some {A} (f : option A → option A) (m : M A) i j x : partial_alter f i m !! j = Some x ↔ (i = j ∧ f (m !! i) = Some x) ∨ (i ≠ j ∧ m !! j = Some x).
proof: Proof. destruct (decide (i = j)); subst. - rewrite lookup_partial_alter. naive_solver. - rewrite lookup_partial_alter_ne; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)