proposition: Lemma find_eta f1 f2 : valid f1 -> valid f2 -> (forall k, find k f1 = find k f2) -> f1 = f2.
proof: Proof. rewrite !pcmE /= !umEX /UM.valid /UM.find -{2 3}[f1]UMC.tfE -{2 3}[f2]UMC.tfE. case: (UMC.from f1) (UMC.from f2)=>[|f1' F1][|f2' F2] // _ _ H. by rewrite !umEX; apply/fmapP=>k; move: (H k); rewrite !umEX. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)