proposition: Lemma path_omap a f x : path ord x (dom f) -> path ord x (dom (omap a f)).
proof: Proof. apply: subseq_path; first by apply: trans. apply: (sorted_subset_subseq (ltT := ord)); last by apply: dom_omap_sub. - by apply: irr. - by apply: trans. - by apply: sorted_dom. by apply: sorted_dom. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)