proposition: Lemma ummonoF f x : um_mono f -> um_mono (free f x).
proof: Proof. move/ummonoP=>X; apply/ummonoP=>k k' v v'. by case/InF=>_ _ F /InF [_ _]; apply: X F. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)