proposition: Lemma dom_omfPtUn f t e h : dom (f (pts t e \+ h)) =i [pred x | valid (pts t e \+ h) & (map_fun f (t, e) && (x == t)) || (x \in dom (f h))].
proof: Proof. move=>x; rewrite dom_omfUn // !inE; case V: (valid (pts t e \+ h))=>//. have T : C t by apply: validPtUn_cond V. rewrite omfPt //; case E: (map_fun _ _)=>[a|] /=. - by rewrite domPt inE T eq_sym. by rewrite dom0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)