proposition: Lemma prec_filtV x1 x2 y1 y2 : valid (x1 \+ y1) -> x1 \+ y1 = x2 \+ y2 -> reflect (x1 = um_filterk (mem (dom x1)) x2) (valid (x1 \+ y2)).
proof: Proof. move=>V1 E; case X : (valid (x1 \+ y2)); constructor; last first. - case: (prec_domV V1 E) X=>// St _ H; apply: St. by move=>n; rewrite H dom_umfiltk inE; case/andP. move: (umfiltk_dom V1); rewrite E umfiltUn -?E //. rewrite (eq_in_umfiltk (f:=y2) (p2:=pred0)). - by rewrite umfilt_pred0 ?unitR //; rewrite E in V1; rewrite (validE2 V1). by move=>n; case: validUn X=>// _ _ L _ /(contraL (L _)) /negbTE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)