proposition: Lemma eqlz_seprel_ax : seprel_axiom ('eqlz f1 f2).
proof: Proof. rewrite /eqlz; split=>[|x y W|x y W|x y z W]. - by rewrite !sep00 !pfunit eq_refl. - by rewrite !andbA andbAC (sepC D1) // (sepC D2). - by case/and4P=>V1 V2 -> _; rewrite (sepx0 W V1) (sepx0 W V2) !pfunit eq_refl. case/and4P=>V1 V2 Ex Ey /and4P [W1 W2 _ Ez]. set j1 := (sepAxx W V1 W1); set j2 := (sepAxx W V2 W2). by rewrite !pfjoin ?j1 ?j2 ?(validLE3 W) //= Ex (eqP Ey) (eqP Ez) !eq_refl. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)