proposition: Lemma umem_eq f1 f2 : valid f1 -> valid f2 -> (forall x, x \In f1 <-> x \In f2) -> f1 = f2.
proof: Proof. move=>V1 V2 H; apply: find_eta=>// k. case K1 : (find k f1)=>[a1|]; case K2 : (find k f2)=>[a2|] //. - by move/In_find/H/In_find: K1; rewrite K2. - by move/In_find/H/In_find: K1; rewrite K2. by move/In_find/H/In_find: K2; rewrite K1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)