proposition: Lemma valid_freshUn h1 h2 v : valid h1 -> [pcm h2 <= h1] -> valid (fresh h1 \-> v \+ h2) = valid h2.
proof: Proof. move=>V [x E]; rewrite {h1}E in V *. by rewrite validPtUn dom_freshUn // andbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)