proposition: Lemma index_mem_dom_range f k t : (k, t) \In f -> uniq (range f) -> index k (dom f) = index t (range f).
proof: Proof. rewrite /range assocs_dom. elim/um_indf: f k t=>[||k' t' f IH W /(order_path_min (@trans K)) P] k t. - by move/In_undef. - by move/In0. rewrite assocsPtUn // !map_cons /= InPtUnE //=. case=>[[->->]|H1 H2]; first by rewrite !eq_refl. case: eqP (In_dom H1) W=>[-> D|_ _ W]. - by rewrite validPtUn D !andbF. case: eqP (In_range H1) H2=>[-> /mem_seqP ->//|_ _ /andP [H2 H3]]. by rewrite (IH _ _ H1). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)