proposition: Lemma kmap_partial_alter {A} (g : option A → option A) (m : M1 A) i : kmap f (partial_alter g i m) = partial_alter g (f i) (kmap f m).
proof: Proof. apply map_eq; intros j. apply option_eq; intros y. destruct (decide (j = f i)) as [->|?]. { by rewrite lookup_partial_alter, !lookup_kmap, lookup_partial_alter. } rewrite lookup_partial_alter_ne, !lookup_kmap_Some by done. split. - intros [i' [? Hm]]; simplify_eq/=. rewrite lookup_partial_alter_ne in Hm by naive_solver. naive_solver. - intros [i' [? Hm]]; simplify_eq/=. exists i'. rewrite lookup_partial_alter_ne by naive_solver. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)