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