proposition: Lemma freePt2 k1 k2 v : C k2 -> free (pts k2 v : U) k1 = if k1 == k2 then Unit else pts k2 v.
proof: Proof. by move=>N; rewrite ptsU freeU free0 N. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)