proposition: Lemma solved_var_inc_list : forall x y z l, z <> y -> VSet.mem z (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)) -> VSet.mem z (set_of_variables_in_unsolved_part l).
proof: Proof. intros x y z l z_diff_y z_in_l'; induction l as [ | [s t] l]; trivial; destruct_set z_in_l' z_in_s'_t' z_in_l''. destruct_set z_in_s'_t' z_in_s' z_in_t'. simpl set_of_variables_in_unsolved_part; do 2 apply VSet.union_1; apply solved_var_inc_term with x y; trivial. simpl set_of_variables_in_unsolved_part; apply VSet.union_1; apply VSet.union_2; apply solved_var_inc_term with x y; trivial. simpl set_of_variables_in_unsolved_part; apply VSet.union_2; 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)