proposition: Lemma In_dom0 A (h : natmap A) k e : (k, e) \In h -> k \in 0::dom h.
proof: Proof. by move=>H; rewrite inE (In_dom H) orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)