proposition: Lemma dom_inverse f : valid (inverse f) -> dom (inverse f) =i range f.
proof: Proof. rewrite /inverse/um_foldl/range; case: ifP=>_; last by rewrite valid_undef. elim: (assocs f)=>[|x g IH] /= W k; first by rewrite dom0. rewrite foldl_init in W *; last by move=>*; rewrite joinAC. by rewrite domUnPt !inE W /= eq_sym IH // (validL W). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)