proposition: Lemma umem_eqD f1 f2 : valid f1 -> valid f2 -> dom f1 =i dom f2 -> (forall x, x \In f1 -> x \In f2) -> f1 = f2.
proof: Proof. move=>V1 V2 E H; apply: umem_eq=>//; case=>k v; split; first by apply: H. move=>H2; move: (In_dom H2); rewrite -E /= =>/In_domX [w H1]. by move/H/(In_fun H2): (H1)=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)