proposition: Lemma omapF k (f : U) : omap a (free f k) = free (omap a f) k :> U'.
proof: Proof. case W : (valid f); last first. - by move/negbT/invalidE: W=>->; rewrite free_undef omap_undef free_undef. apply: umem_eq. - by rewrite valid_omap // validF. - by rewrite validF valid_omap. case=>x v; split. - case/In_omapX=>v' /InF /= [_ N M E]. apply/InF; rewrite validF valid_omap //=; split=>//. by apply/In_omapX; exists v'. case/InF=>/= _ N /In_omapX [v'] M E. by apply/In_omapX; exists v'=>//; apply/InF; rewrite validF. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)