proposition: Lemma solved_var_inc_not_mem : forall x y t, x <> y -> ~ VSet.mem x (set_of_variables (apply_subst ((x, Var y) :: nil) t)).
proof: Proof. intros x y t x_diff_y; pattern t; apply T.term_rec3. intros 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]. intros [x_eq_y | x_in_nil] ; [apply x_diff_y; subst; trivial | contradiction]. intros [x_eq_v | x_in_nil]. unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A, DecVar.eq_A in *; subst; apply v_diff_x; trivial. contradiction. intros f l IHl x_in_l'; simpl in x_in_l'; clear f; induction l as [ | s l]; trivial. simpl in x_in_l'; destruct_set x_in_l' x_in_s' x_in_l''. apply (IHl s); trivial; left; trivial. apply IHl0; trivial. intros; apply IHl; 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)