proposition: Lemma dom_fresh_sub A1 A2 (h1 : natmap A1) (h2 : natmap A2) : valid h1 -> {subset dom h2 <= dom h1} -> fresh h1 \notin dom h2.
proof: Proof. move=>V S; apply: contra; first by move/S; apply: dom_ordfresh. by rewrite ltnn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)