proposition: Lemma inv_idfun (U : pcm) : inv_morph [morphism of @idfun U].
proof: Proof. by split=>// a b1 b2 V _ E; exists b1, b2; rewrite -E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype) pcm(options axioms prelude) pcm(pcm morphism)