proposition: Lemma nm_dom0 A (h : natmap A) : (h = undef \/ h = Unit) <-> (dom h = [::]).
proof: Proof. split=>[|E]; first by case=>->; rewrite ?dom_undef ?dom0. case V : (valid h); last by move/invalidE: (negbT V)=>->; left. by rewrite (dom0E V) ?E //; right. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)