proposition: Lemma dom_freshUnK h1 h2 v : valid h1 -> [pcm h2 <= h1] -> dom (fresh h1 \-> v \+ h2) = rcons (dom h2) (fresh h1).
proof: Proof. move=>V [x E]; subst h1; rewrite joinC domUnPtK //. - by rewrite joinC valid_freshUn // (validL V). apply/allP=>k /= D; apply: dom_ordfresh. by rewrite domUn inE V D. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)