proposition: Lemma solved_var_inc_not_mem_subst : forall x y sigma, x <> y -> ~VSet.mem x (set_of_variables_in_range_of_subst (map_subst (fun (_ : variable) (v_sigma : term) => apply_subst ((x, Var y) :: nil) v_sigma) sigma)).
proof: Proof. intros x y sigma x_diff_y x_in_sigma'; induction sigma as [ | [v t] sigma]. contradiction. simpl set_of_variables_in_range_of_subst in x_in_sigma'; destruct_set x_in_sigma' x_in_t' x_in_sigma''. apply (solved_var_inc_not_mem _ _ _ x_diff_y x_in_t'). apply IHsigma; 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)