proposition: Lemma umpfx_undef h : um_prefix undef h.
proof: Proof. by rewrite /um_prefix assocs_undef; apply/prefixE; exists (assocs h). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)