proposition: Lemma assocsUn (h1 h2 : U) : valid (h1 \+ h2) -> (forall k1 k2, k1 \in dom h1 -> k2 \in dom h2 -> ord k1 k2) -> assocs (h1 \+ h2) = assocs h1 ++ assocs h2.
proof: Proof. move: h1 h2; apply: um_indf=>[h1|h2 W H| k v f IH W1 /(order_path_min (@trans _)) P h2 W2 H]. - by rewrite undef_join valid_undef. - by rewrite assocs0 unitL. rewrite -joinA in W2; rewrite -joinA !assocsPtUn //= ?IH //. - by rewrite (validR W2). - by move=>k1 k2 K1 K2; apply: H=>//; rewrite domPtUn inE K1 orbT W1. apply/allP=>x; rewrite domUn inE (validR W2) /=. by case/orP=>[/(allP P)//|]; apply: H; rewrite domPtUnE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)