proposition: Lemma dom_prec f1 f2 g1 g2 : valid (f1 \+ g1) -> f1 \+ g1 = f2 \+ g2 -> dom f1 =i dom f2 -> f1 = f2.
proof: Proof. rewrite -{4}[f1]UMC.tfE -{3}[f2]UMC.tfE !pcmE /= !umEX. rewrite /UM.valid /UM.union /UM.dom; move=>D E. case: (UMC.from f1) (UMC.from f2) (UMC.from g1) (UMC.from g2) E D=> [|f1' F1][|f2' F2][|g1' G1][|g2' G2] //; case: ifP=>// D1; case: ifP=>// D2 E _ E1; apply/fmapP=>k. move/(_ k): E1=>E1. case E2: (k \in supp f2') in E1; last first. - by move/negbT/fnd_supp: E1=>->; move/negbT/fnd_supp: E2=>->. suff L: forall m s, k \in supp m -> disj m s -> fnd k m = fnd k (fcat m s) :> option V. - by rewrite (L _ _ E1 D1) (L _ _ E2 D2) E. by move=>m s S; case: disjP=>//; move/(_ _ S)/negbTE; rewrite fnd_fcat=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)