proposition: Lemma um_eta k f : k \in dom f -> exists v, find k f = Some v /\ f = pts k v \+ free f k.
proof: Proof. case: dom_find=>// v E1 E2 _; exists v; split=>//. by rewrite {1}E2 -{1}[free f k]unitL updUnR domF inE /= eq_refl ptsU. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)