proposition: Lemma omg_eta_all (h : natmap (bool * bool)) : valid h -> omg h = own -> um_all (fun k v => v.2 = ~~ v.1) h -> exists h', [/\ h' = free h (last_key h), h = last_key h \-> (false, true) \+ h', last_key h != 0, last_key h \in dom h, last_key h \notin dom h' & last_key h' < last_key h].
proof: Proof. move=>V H A; case: (omg_eta V H)=>h' [v][H1 H2 H3 H4 H5 H6]. exists h'; split=>//; rewrite H2 in V A; case: (umallPtUnE V A)=>/=. by case: v {A} V H2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)