proposition: Lemma umpfxI h1 h2 : valid (h1 \+ h2) -> (forall x y, x \in dom h1 -> y \in dom h2 -> ord x y) -> um_prefix h1 (h1 \+ h2).
proof: Proof. by move=>W X; rewrite /um_prefix assocsUn //; 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)