proposition: Lemma domeq2_omap (a : K*V -> option V') f : (forall kv, kv \In f -> isSome (a kv)) -> dom_eq2 (omap a f) f.
proof: Proof. move=>H; rewrite /dom_eq2 valid_omap // eq_refl /=. apply/eqP; apply: ord_sorted_eq=>// k. apply/idP/idP; first by case/In_dom_omap=>// x [w][] /In_dom. case/In_domX=>x X; apply/In_dom_omap=>//. by case F : (a (k, x)) (H _ X)=>[v|] //; exists v, x. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)