proposition: Lemma In_fresh V (h : natmap V) x e t k : fresh h <= t -> (k, x) \In h -> (k, x) \In t \-> e \+ h.
proof: Proof. by move=>N H; apply/InR=>//; rewrite valid_fresh // (In_valid H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)