proposition: Lemma joinX (U V : pcm) D1 D2 (f1 : @morphism U V D1) (f2 : @morphism U V D2) x : 'join f1 f2 x = f1 x \+ f2 x.
proof: Proof. by []. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)