proposition: Lemma domK f1 f2 g1 g2 : valid (f1 \+ g1) -> valid (f2 \+ g2) -> dom (f1 \+ g1) =i dom (f2 \+ g2) -> dom f1 =i dom f2 -> dom g1 =i dom g2.
proof: Proof. rewrite !pcmE /= !umEX /UM.valid /UM.union /UM.dom. case: (UMC.from f1) (UMC.from f2) (UMC.from g1) (UMC.from g2)=> [|f1' F1][|f2' F2][|g1' G1][|g2' G2] //. case: disjP=>// D1 _; case: disjP=>// D2 _ E1 E2 x. move: {E1 E2} (E2 x) (E1 x); rewrite !supp_fcat !inE /= => E. move: {D1 D2} E (D1 x) (D2 x)=><- /implyP D1 /implyP D2. case _ : (x \in supp f1') => //= in D1 D2 *. by move/negbTE: D1=>->; move/negbTE: D2=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)