proposition: Lemma inverse_idemp (f : U) : valid (inverse f : U') -> inverse (inverse f : U') = f.
proof: Proof. move=>W; apply/umem_eq. - by rewrite valid_inverse_idemp. - by move: W; rewrite valid_inverse; case/and3P. move=>x; split=>H. - by apply/(In_inverse _ _ W); apply/(@In_inverse _ _ _ _ _ U) =>//; case: H. case: x H=>k v /(In_inverse _ _ W)/In_inverse; apply. by rewrite valid_inverse_idemp. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)