proposition: Lemma foldf_ins g e k v f: path ord k (supp f) -> foldfmap g e (ins k v f) = g (k, v) (foldfmap g e f).
proof: Proof. by move=> H; rewrite /foldfmap //= seqof_ins //. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)