proposition: Lemma xpsub_morphP : morph_axiom D xpsub.
proof: Proof. rewrite /xpsub; split=>[|x y W E]. - by apply: xval_inj; case: decP=>//; rewrite pfunit /= valid_unit sep00. case: decP=>Hx; last by rewrite (sep0E W E) (validE2 W) in Hx. case: decP=>Hy; last by rewrite (sep0E W E) (validE2 W) in Hy. case: decP=>H; last by rewrite W (sepU0 W E) in H. rewrite /valid /= /xsep_valid /= !pcm_joinE /= /xsep_join /= !unlock /= /xsep_join' /=. rewrite {1 2}W {1 2}E {1}W {1}(sepU0 W E) /=. by split=>//; apply: xval_inj; rewrite /= /xsep_join' W E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)