proposition: Lemma dom_fresh t1 e h : valid h -> fresh h <= t1 -> dom (t1 \-> e \+ h) = rcons (dom h) t1.
proof: Proof. move=>W N; rewrite joinC domUnPtK //. - by rewrite joinC valid_fresh. by apply/allP=>x /dom_ordfresh D; apply: leq_ltn_trans N. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)