proposition: Lemma In_fun k v1 v2 f : (k, v1) \In f -> (k, v2) \In f -> v1 = v2.
proof: Proof. by move/In_find=>H1 /In_find; rewrite H1; case. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)