proposition: Lemma valid_psub x : valid (psub x) = valid x && D x Unit.
proof: Proof. by rewrite -{2}[x]unitR -valid_psubU pfunit unitR. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)