proposition: Lemma unionmap_eqP : Equality.axiom unionmap_eq.
proof: Proof. move=>x y; rewrite -{1}[x]UMC.tfE -{1}[y]UMC.tfE /unionmap_eq. case: (UMC.from x)=>[|f1 H1]; case: (UMC.from y)=>[|f2 H2] /=. - by constructor. - by constructor; move/(@UMC.eqE _ _ _ (UMC T m)). - by constructor; move/(@UMC.eqE _ _ _ (UMC T m)). case: eqP=>E; constructor; rewrite (@UMC.eqE _ _ _ (UMC T m)). - by rewrite UM.umapE. by case. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)