proposition: Lemma rangeF k (f : U) : {subset range (free f k) <= range f}.
proof: Proof. case W: (valid f); last first. - by move/negbT/invalidE: W=>->; rewrite free_undef !range_undef. case D: (k \in dom f); last by move/negbT/dom_free: D=>->. case: (um_eta D) W=>x [_] {1 3}-> Vf p. by rewrite rangePtUn inE Vf=>->; rewrite orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)