proposition: Lemma domeqUP A1 A2 x (xs1 : seq A1) (xs2 : seq A2) : size xs1 = size xs2 -> dom_eq (updi x xs1) (updi x xs2).
proof: Proof. move=>E; apply/domeqP; split; first by rewrite !updiD E. move=>z; case: updiP=>[[H][m][->]|X]; first by rewrite updimV H E. by case: updiP=>// [[H]][m][Ez S]; elim: X; split=>//; exists m; rewrite Ez E. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)