proposition: Lemma xpsub_xval x : xpsub (xval x) = x.
proof: Proof. by apply: xval_inj; rewrite /xpsub; case: decP; case: x=>// x []. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)