proposition: Lemma inv_eqlz U (V : eqpcm) (D1 D2 : sep_rel U) (f : morphism V D1) (g : morphism V D2) : (forall x x1 x2 : EQPCM.pcm V, valid (x \+ x1) -> x \+ x1 = x \+ x2 -> x1 = x2) -> inv_rel D1 -> inv_rel D2 -> inv_rel ('eqlz f g).
proof: Proof. move=>K HD1 HD2 x y z W; rewrite !sepE /=. case/and4P=>X1 X2 Ex _ /and4P [Y1 Y2] Ey /eqP. case/andP: (HD1 _ _ _ W X1 Y1)=>E1 E1'. case/andP: (HD2 _ _ _ W X2 Y2)=>E2 E2'. rewrite E1 E2 Ex Ey E1' E2' !pfjoin ?(validLE3 W) 2?(sepAxx W) //=. rewrite -(eqP Ex) (eqP Ey) eq_refl=>/K ->; first by rewrite eq_refl. by rewrite pfV2 // ?(validLE3 W)// (sepAxx W). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype) pcm(options axioms prelude) pcm(pcm morphism)