proposition: Lemma freeX k v f1 f2 : valid f1 -> f1 = pts k v \+ f2 -> f2 = free f1 k.
proof: Proof. by move=>W E; rewrite E freePtUn // -E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)