proposition: Lemma inv_comp (U V W : pcm) (C : sep_rel V) (D : sep_rel U) (f : morphism V D) (g : morphism W C) : inv_morph g -> inv_morph f -> inv_morph [morphism of g \o f].
proof: Proof. case=>HC Hg [HD Hf]; split=>[a1 a2 a' V1|a b1 b2 V1] /andP []. - move=>/(HD _ _ _ V1) H1 H2 /andP [/H1] /andP [D1 D2]. rewrite !sepE !pfjoin ?(validLE3 V1, sepAxx V1 D1 D2) //= in H2 *. by apply: HC H2; apply: pfV3. move=>D1; rewrite pfunit=>C1. case/(Hg _ _ _ (pfV f V1 D1) C1)=>c1 [c2][Ef Vc Xc <-<-]. case/(Hf _ _ _ V1 D1): Ef Xc=>a1 [a2][-> Va Xc <-<- Xd]. by exists a1, a2; rewrite !sepE Xc Xd. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype) pcm(options axioms prelude) pcm(pcm morphism)