proposition: Lemma um_eta2 k v f : find k f = Some v -> f = pts k v \+ free f k.
proof: Proof. by move=>E; case/um_eta: (find_some E)=>v' []; rewrite E; case=><-. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)