proposition: Lemma freeF k1 k2 f : free (free f k2) k1 = if k1 == k2 then free f k1 else free (free f k1) k2.
proof: Proof. rewrite !umEX /UM.free. by case: (UMC.from f)=>[|f' F]; case: ifP=>// E; rewrite !umEX rem_rem E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)