proposition: Lemma join_morph_ax : morph_axiom ('sep_join f1 f2) ('join f1 f2).
proof: Proof. rewrite /join; split=>[|x y]; first by rewrite !pfunit unitL. move=>W /and3P [V1 V2]; rewrite !pfjoin // !joinA. by rewrite !(pull (f2 x)) !joinA !(pull (f1 x)). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)