proposition: Lemma umall2PtUn k v1 v2 f1 f2 : Reflexive P -> Transitive P -> valid f1 = valid f2 -> um_all2 f1 f2 -> P v1 v2 -> um_all2 (pts k v1 \+ f1) (pts k v2 \+ f2).
proof: Proof. move=>R T; case W : (valid (pts k v1 \+ f1)). - move=>H1 H2 H3; apply: umall2Un=>//. - by rewrite !validPt (validPtUn_cond W). by apply/(@umall2Pt _ _ _ (validPtUn_cond W)). case: validUn W=>//. - rewrite validPt=>H _ _ _ _. have L v : pts k v = undef :> U by apply/pts_undef. by rewrite !L !undef_join; apply: umall2_undef. - move=>W _; rewrite (negbTE W)=>/esym. move/invalidE: W=>-> /negbT/invalidE -> _ _; rewrite !join_undef. by apply: umall2_undef. move=>x; rewrite domPt inE=>/andP [X /eqP <- D1] _ W /umall2_dom E _. suff : ~~ valid (pts k v1 \+ f1) /\ ~~ valid (pts k v2 \+ f2). - by case=>/invalidE -> /invalidE ->; apply: umall2_undef. by rewrite !validPtUn X -W -E D1 (dom_valid D1). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)