proposition: Lemma lastval_mem kv h : kv \In h -> exists r, last_val h = Some r.
proof: Proof. by case: lastvalP=>[r|_ H /H//]; exists r. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)