proposition: Lemma freePt k v : C k -> free (pts k v : U) k = Unit.
proof: Proof. by move=>N; rewrite freePt2 // eq_refl. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)