proposition: Lemma all_range_inverse f : all C (range (inverse f)).
proof: Proof. apply: (@sub_all _ (fun k => k \in dom f)); first by move=>x /dom_cond. by apply/allP=>x H; rewrite -range_inverse //; apply: range_valid H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)