proposition: Lemma InF x k f : x \In free f k <-> [/\ valid (free f k), x.1 != k & x \In f].
proof: Proof. case: x=>x1 v1; split; last first. - by case=>W /= N /In_find E; apply/In_find; rewrite findF (negbTE N). case=>W /= H; rewrite W; case: H=>z E. have : find x1 (pts x1 v1 \+ z) = Some v1 by rewrite findPtUn // -E. by rewrite -E findF; case: eqP=>//= _ /In_find. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)