proposition: Lemma solved_var_inc_subst : forall x y z sigma, z <> y -> VSet.mem z (set_of_variables_in_range_of_subst (map_subst (fun (_ : variable) (v_sigma : term) => apply_subst ((x, Var y) :: nil) v_sigma) sigma)) -> VSet.mem z (set_of_variables_in_range_of_subst sigma).
proof: Proof. intros x y z sigma z_diff_y z_in_sigma'; induction sigma as [ | [v t] sigma]; trivial. destruct_set z_in_sigma' z_in_t' z_in_sigma''. simpl set_of_variables_in_range_of_subst; apply VSet.union_1; apply solved_var_inc_term with x y; trivial. simpl set_of_variables_in_range_of_subst; apply VSet.union_2; 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)