proposition: Lemma set_of_var_list_of_var : forall v t, VSet.mem v (set_of_variables t) <-> var_in_term v t = true.
proof: Proof. intros v t; pattern t; apply term_rec3; clear t. intros x; unfold VSet.mem; simpl; unfold DecVar.eq_A. generalize (X.eq_bool_ok x v); case (X.eq_bool x v); [intro v_eq_x; subst v | intro v_diff_x]. intuition. intuition. intros f l IH; simpl. induction l as [ | t l]; simpl. unfold VSet.mem; simpl; intuition. split; intro H. destruct (VSet.union_12 _ _ _ H) as [H1 | H2]. rewrite (IH t (or_introl _ (eq_refl _))) in H1. rewrite var_in_term_list_equation. destruct t as [w | g k]; simpl in H1; simpl. generalize (X.eq_bool_ok v w); case (X.eq_bool v w); [intros _; trivial | intro v_diff_w]. apply False_rect; apply v_diff_w. generalize (X.eq_bool_ok w v); rewrite H1; intro; symmetry; assumption. rewrite H1; trivial. rewrite IHl in H2. rewrite var_in_term_list_equation. destruct t as [w | g k]; simpl. generalize (X.eq_bool_ok v w); case (X.eq_bool v w); [intros _; trivial | intro v_diff_w]. rewrite H2; rewrite Bool.orb_true_r; trivial. rewrite H2; rewrite Bool.orb_true_r; trivial. intros u u_in_l; apply IH; right; trivial. rewrite var_in_term_list_equation in H. destruct t as [w | g k]; simpl in H; simpl. revert H; generalize (X.eq_bool_ok v w); case (X.eq_bool v w); [intros v_eq_w _; subst w | intros v_diff_w H]. apply VSet.union_1; simpl; left; reflexivity. apply VSet.union_2; rewrite IHl; trivial. intros u u_in_l; apply IH; right; trivial. case_eq (var_in_term_list v k); intro v_in_k; rewrite v_in_k in H; simpl in H. apply VSet.union_1. rewrite (IH _ (or_introl _ (eq_refl _))); trivial. apply VSet.union_2. rewrite IHl; trivial. intros u u_in_l; apply IH; right; trivial. Qed.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)