proposition: Lemma liftPJ (x y : lift A) : liftjoin_spec x y (x \+ y) x y.
proof: Proof. by case: x y=>[|x][|y]; rewrite ?downE; constructor. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype) pcm(options prelude) pcm(pcm morphism)