proposition: Lemma supp_mapf (s : finMap K U) : supp (mapf s) = supp s.
proof: Proof. case: s; rewrite /supp /mapf /mapf' /=. by elim=>[|[k v] s IH] //= /path_sorted {}/IH ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)