proposition: Lemma umpleq_atval v t h1 h2 : gapless h1 -> valid h2 -> [pcm h1 <= h2] -> t <= last_key h1 -> atval v t h2 = atval v t h1.
proof: Proof. move=>G V H K; case/(gapless_pleq G V): {V} H (V)=>h [->{h2} H] V. by apply: atvalUn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)