proposition: Lemma solved_var_inc_term : forall x y z t, z <> y -> VSet.mem z (set_of_variables (apply_subst ((x, Var y) :: nil) t)) -> VSet.mem z (set_of_variables t).
proof: Proof. intros x y z t z_diff_y; pattern t; apply T.term_rec3. intro v; simpl; generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x; subst v | intro v_diff_x; trivial]. intros [z_eq_y | z_in_nil]. unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *; subst z; absurd (y=y); trivial. contradiction. intros f l; simpl; fold set_of_variables_list; clear f; induction l as [ | s l]; [trivial | idtac]. intros H_s_l z_in_s'_l'; destruct_set z_in_s'_l' z_in_s' z_in_l'. simpl; apply VSet.union_1; apply H_s_l; trivial; left; trivial. simpl; apply VSet.union_2; apply IHl; trivial. intros; apply H_s_l; [right | idtac] ; 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)