proposition: Lemma countN_varfree i v t : count (pred1 v) (vars t) > 1 -> def (interp i t) -> hlook i v = Some empty.
proof: Proof. elim: t v=>[//|[x d|h] s IH] v H; rewrite interp_cons=>D. - by apply: IH=>//; apply defUnr in D. rewrite /= in H. case: (h =P v) H=>[<-|_]; last by move/IH; apply; apply: defUnr D. case H2: (count _ _)=>[//|[|n]] _; last first. - by apply: IH; [rewrite H2 | apply: defUnr D]. move/count1_hfree: H2=>H2. rewrite -(interp_perm i H2) interp_cons unA in D. move: (defUnl D); rewrite defUnhh /=. by case: (onth _ _)=>// a; move/empP=>->. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)