proposition: Lemma validUnU k v f1 f2 : k \in dom f2 -> valid (f1 \+ upd k v f2) = valid (f1 \+ f2).
proof: Proof. move=>D; apply/esym; move: D; case: validUn. - by move=>V' _; apply/esym/negbTE; apply: contra V'; move/validL. - move=>V' _; apply/esym/negbTE; apply: contra V'; move/validR. by rewrite validU; case/andP. - move=>k' H1 H2 _; case: validUn=>//; rewrite validU => D1 /andP [/= H D2]. by move/(_ k' H1); rewrite domU !inE H D2 H2; case: ifP. move=>V1 V2 H1 H2; case: validUn=>//. - by rewrite V1. - by rewrite validU V2 (dom_cond H2). move=>k'; rewrite domU (dom_cond H2) inE /= V2; move/H1=>H3. by rewrite (negbTE H3); case: ifP H2 H3=>// /eqP ->->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)