proposition: Lemma lastkeyUn0T A1 A2 (h1 : natmap A1) (h2 : natmap A2) : valid h1 -> valid h2 -> (forall x, x \in dom h1 -> x \in dom h2 -> false) -> last_key h1 = last_key h2 -> (h1 = Unit) * (h2 = Unit).
proof: Proof. move=>V1 V2 D E. case E1: (unitb h1). - move/unitbE: E1 E V2=>->; rewrite lastkey0. by case/esym/dom_lastkey0P/nm_dom0=>-> //; rewrite valid_undef. case E2: (unitb h2). - move/unitbE: E2 E V1=>->; rewrite lastkey0. by case/dom_lastkey0P/nm_dom0=>-> //; rewrite valid_undef. move: (D _ (dom_lastkey V1 (negbT E1))). by rewrite E (dom_lastkey V2 (negbT E2))=>/(_ erefl). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)