proposition: Lemma umpfxD h1 h2 : um_prefix h1 h2 -> prefix (dom h1) (dom h2).
proof: Proof. by case/prefixE=>x E; rewrite !assocs_dom E map_cat; apply: prefix_cat. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)