fact: Fixpoint set_of_variables_in_unsolved_part (l : list (term * term)) : VSet.t := match l with | nil => VSet.empty | (s,t) :: l => VSet.union (VSet.union (set_of_variables s) (set_of_variables t)) (set_of_variables_in_unsolved_part l) end.
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)