proposition: Lemma dom_freshUnN h1 h2 x : valid h1 -> [pcm h2 <= h1] -> x \in dom h2 -> x != fresh h1.
proof: Proof. by move=>V H; apply: contraL=>/eqP ->; apply: dom_freshUn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)