proposition: Lemma validUn f1 f2 : validUn_spec f1 f2 (valid (f1 \+ f2)).
proof: Proof. rewrite !pcmE /= !umEX -{1}[f1]UMC.tfE -{1}[f2]UMC.tfE. rewrite /UM.valid /UM.union /=. case: (UMC.from f1) (UMC.from f2)=>[|f1' F1][|f2' F2] /=. - by apply: valid_false1; rewrite pcmE /= !umEX. - by apply: valid_false1; rewrite pcmE /= !umEX. - by apply: valid_false2; rewrite pcmE /= !umEX. case: ifP=>E. - apply: valid_true; try by rewrite !pcmE /= !umEX. by move=>k; rewrite !umEX => H; case: disjP E=>//; move/(_ _ H). case: disjP E=>// k T1 T2 _. by apply: (valid_false3 (k:=k)); rewrite !umEX. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)