proposition: Lemma In_fresh_inv V (h : natmap V) x e t k : k < fresh h -> fresh h <= t -> (k, x) \In t \-> e \+ h -> (k, x) \In h.
proof: Proof. move=>N F H; have W : valid (t \-> e \+ h). - by rewrite valid_fresh // (validR (In_valid H)). by case/(InPtUnE _ W): H F=>// [[<- _]]; case: ltngtP N. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)