proposition: Lemma xval_xpsub x : valid x -> D x Unit -> xval (xpsub x) = x.
proof: Proof. by rewrite /xpsub /= => W H; case: decP=>//=; rewrite W H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)