proposition: Lemma map_fold_singleton {A B} (f : K → A → B → B) (b : B) i x : map_fold f b {[i:=x]} = f i x b.
proof: Proof. apply (map_fold_foldr _ [(i,x)]); [solve_proper|..]. - intros j1 j2 z1 z2 y ?. rewrite !lookup_singleton_Some. naive_solver. - by rewrite map_to_list_singleton. Qed.
imports: Coq(Permutation) stdpp(options)