proposition: Lemma uniq_rangeP f : reflect (forall k1 k2 v, (k1, v) \In f -> (k2, v) \In f -> k1 = k2) (uniq (range f)).
proof: Proof. case W : (valid f); last first. - move/negbT/invalidE: W=>->; rewrite range_undef. by constructor=>k1 k2 v /In_undef. case H : (uniq (range f)); constructor; last first. - move=>H'; move/negbT/negP: H; elim. rewrite map_inj_in_uniq; first by apply: uniq_assocs. case=>/= k1 v [k2 v'] /mem_seqP/In_assocs H1 /mem_seqP/In_assocs H2 /= H3. by rewrite -H3 in H2 *; rewrite (H' _ _ _ H1 H2). move/uniqP: H=>H k1 k2 v H1 H2. set j1 := index k1 (dom f). set j2 := index k2 (dom f). have [D1 D2] : k1 \in dom f /\ k2 \in dom f. - by move/In_dom: H1; move/In_dom: H2. have [R1 R2] : j1 < size (assocs f) /\ j2 < size (assocs f). - by rewrite size_assocs !index_mem. have [M1 M2] : j1 < size (dom f) /\ j2 < size (dom f). - by rewrite !index_mem. have [A1 A2] : (k1, v) \in assocs f /\ (k2, v) \in assocs f. - by move/In_assocs/mem_seqP: H1=>->; move/In_assocs/mem_seqP: H2=>->. have InjF : {in assocs f &, injective fst}. - case=>a1 v1 [a2 v2] /mem_seqP X1 /mem_seqP X2 /= E. by move: E X1 X2 => -> X1 /(assocs_map X1) ->. have /eqP E1 : j1 == index (k1,v) (assocs f). - rewrite -(nth_uniq (k1,v) R1 _ (uniq_assocs _)); last by rewrite index_mem. by rewrite /j1 assocs_dom (nth_index_map _ InjF A1) nth_index. have /eqP E2 : j2 == index (k2,v) (assocs f). - rewrite -(nth_uniq (k2,v) R2 _ (uniq_assocs _)); last by rewrite index_mem. by rewrite /j2 assocs_dom (nth_index_map _ InjF A2) nth_index. have E : nth v (range f) j1 = nth v (range f) j2. - rewrite /range (nth_map (k1,v) v _ R1) (nth_map (k2,v) v _ R2). by rewrite E1 E2 !nth_index. have : j1 = j2 by apply: H E; rewrite inE size_range. by move/eqP; rewrite -(nth_uniq k1 M1 M2 (uniq_dom _)) !nth_index // =>/eqP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)