proposition: Lemma inv_ker U (V : tpcm) (D : sep_rel U) (f : morphism V D) : inv_rel D -> inv_rel ('ker f).
proof: Proof. move=>HD a1 a2 a' W; rewrite !sepE /=. case/and3P=>D1 /unitbP Eq1 _ /and3P [D2 /unitbP Eq2 /unitbP]. case/andP: (HD _ _ _ W D1 D2)=>{}D1 {}D2. rewrite !pfjoin ?(validLE3 W) //; last by rewrite (sepAxx W). by rewrite Eq1 Eq2 D1 D2 !unitL =>->; rewrite tpcmE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype) pcm(options axioms prelude) pcm(pcm morphism)