proposition: Lemma pval_psub x : valid x -> D x Unit -> pval (psub x) = x.
proof: Proof. by case: X=>pval psub [H1 H2 H3 H4]; apply: H3. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)