proposition: Lemma lift_eqP : Equality.axiom lift_eq.
proof: Proof. case=>[|x][|y] /=; try by constructor. by apply: (iffP eqP)=>[->|[]]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype) pcm(options prelude) pcm(pcm morphism)