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