proposition: Lemma lastkeyUn0 A (h1 h2 : natmap A) : valid (h1 \+ h2) -> last_key h1 = last_key h2 -> (h1 = Unit) * (h2 = Unit).
proof: Proof. move=>V E. case: validUn V=>// V1 V2 D _; apply: lastkeyUn0T V1 V2 _ E. by move=>x /D /negbTE ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)