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