proposition: Lemma solved_var_inc_not_mem_list : forall x y l, x <> y -> ~ VSet.mem x (set_of_variables_in_unsolved_part (map (fun uv : term * term => let (u, v) := uv in (apply_subst ((x, Var y) :: nil) u, apply_subst ((x, Var y) :: nil) v)) l)).
proof: Proof. intros x y l x_diff_y x_in_l'; induction l as [ | [s t] l]. contradiction. simpl set_of_variables_in_unsolved_part in x_in_l'; destruct_set x_in_l' x_in_s'_t' x_in_l''. destruct_set x_in_s'_t' x_in_s' x_in_t'. apply (solved_var_inc_not_mem _ _ _ x_diff_y x_in_s'). apply (solved_var_inc_not_mem _ _ _ x_diff_y x_in_t'). apply IHl; 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)