proposition: Lemma var_occurs_in_ok : forall t, var_occurs_in t = true <-> In x (vars t).
proof: Proof. apply term_ind_forall. intro n; simpl. rewrite (beq_nat_ok x n). intuition. intros f v Rfv. rewrite var_occurs_in_fun, vars_fun. induction v. simpl. intuition. simpl in Rfv. destruct Rfv as [Rfa Rfv]. simpl. rewrite orb_eq. split; intros H. apply in_or_app. rewrite <- Rfa, <- IHv; auto. rewrite Rfa, IHv; auto. apply in_app_or. auto. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)