proposition: Lemma map_Forall_fmap {B} (f : B → A) (m : M B) : map_Forall P (f <$> m) ↔ map_Forall (λ k, (P k ∘ f)) m.
proof: Proof. unfold map_Forall. setoid_rewrite lookup_fmap. setoid_rewrite fmap_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)