proposition: Lemma valid_inverse_idemp (f : U) : valid (inverse (inverse f : U') : U) = valid (inverse f : U').
proof: Proof. by rewrite valid_inverse uniq_range_inverse all_range_inverse !andbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)