proposition: Lemma In_inj_fun k v1 v2 f : {in dom f, injective (fun x => find x f)} -> (v1, k) \In f -> (v2, k) \In f -> v1 = v2.
proof: Proof. move=>H H1 H2; apply: H=>//. - by move/In_dom: H1. by move/In_find: H1 H2=>-> /In_find ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)