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