proposition: Lemma fresh_omfT t h : fresh h <= t -> fresh (f h) <= t.
proof: Proof. by apply: leq_trans (fresh_omf _). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)