proposition: Lemma omf_subdom0 B h (f : omap_fun (nat_mapUMC A) (nat_mapUMC B)) : {subset 0::dom (f h) <= 0::dom h}.
proof: Proof. move=>x; rewrite !inE; case/orP=>[->//|]. by move/omf_subdom=>->; rewrite orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)