proposition: Lemma eqlzX (U : pcm) (V : eqpcm) D1 D2 (f1 : @morphism U V D1) (f2 : @morphism U V D2) x y : 'eqlz f1 f2 x y = [&& D1 x y, D2 x y, f1 x == f2 x & f1 y == f2 y].
proof: Proof. by []. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)