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