proposition: Lemma assocs_map K C (V : Type) (U : @union_map_class K C V) (f : U) k v1 v2 : (k, v1) \In assocs f -> (k, v2) \In assocs f -> v1 = v2.
proof: Proof. rewrite !umEX; case: (UMC.from f)=>//= g _; case: g=>g S /= H1 H2. have {S} S' : uniq [seq key i | i <- g]. - by apply: sorted_uniq S; [apply: trans | apply: irr]. have X : forall (g : seq (K*V)) k v, (k, v) \In g -> k \in map fst g. - elim=>[|[ka va] h IH] // kb vb. - rewrite !InE; case; first by case=>-> _; rewrite inE eq_refl. by move/IH; rewrite inE=>->; rewrite orbT. elim: g k v1 v2 S' H1 H2=>[|[ka va] g IH] //= k v1 v2. case/andP=>U1 U2; rewrite !InE. case; first by case=>->->; case=>[[]|/X] //; rewrite (negbTE U1). move=>H1 H2; case: H2 H1. - by case=>->-> /X; rewrite (negbTE U1). by move=>H1 H2; apply: IH H2 H1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)