proposition: Lemma dom_omap_subseq (a1 : K * V -> option V1) (a2 : K * V -> option V2) (f : U) : (forall kv, kv \In f -> isSome (a1 kv) -> isSome (a2 kv)) -> subseq (dom (omap (U':=U1) a1 f)) (dom (omap (U':=U2) a2 f)).
proof: Proof. elim/um_indf: f=>[||k v f IH W P] H. - by rewrite !omap_undef !dom_undef. - by rewrite !omap0 !dom0. rewrite !omapPtUn W; move: (W); rewrite validPtUn=>W'. have T : transitive (T:=K) ord by apply: ordtype.trans. have B : (k, v) \In pts k v \+ f by apply: InPtUnL. case E1 : (a1 (k, v))=>[x1|]. - have /(H _ B) : isSome (a1 (k, v)) by rewrite E1. case: (a2 (k, v))=>// x2 _. rewrite !domPtUnK //=; last first. - by apply/allP=>? /In_dom_omap [?][?][] /In_dom Y _; apply: path_mem Y. - by rewrite valid_omapPtUn. - by apply/allP=>? /In_dom_omap [?][?][] /In_dom Y _; apply: path_mem Y. - by rewrite valid_omapPtUn. by rewrite eq_refl; apply: IH=>kx X; apply: H (InR _ _). case E2 : (a2 (k, v))=>[x2|]; last by apply: IH=>kx X; apply: H (InR _ _). rewrite domPtUnK /=; last first. - by apply/allP=>? /In_dom_omap [?][?][] /In_dom Y _; apply: path_mem Y. - by rewrite valid_omapPtUn. case D : (dom (omap a1 f))=>[//|x xs]. case: eqP D=>[-> D|_ <-]; last by apply: IH=>kv X; apply: H (InR _ _). have : k \in dom (omap (U':=U1) a1 f) by rewrite D inE eq_refl. case/In_dom_omap=>w1 [w2][] /In_dom /= D1. by rewrite validPtUn D1 !andbF in W. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)