proposition: Lemma comp_morph_ax : morph_axiom ('preim f Dv) (g \o f).
proof: Proof. split=>[|x y] /=; first by rewrite !pfunit. by rewrite /preim => D /andP [H1 H2]; rewrite !pfjoin // !pfV2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)