fact: Fixpoint well_sorted_partly_solved_part (l : list (variable * partly_solved_term)) : Prop := match l with | nil => True | (v,p) :: tl => v <> new_var p /\ (forall v', 1 <= nb_occ X.eq_bool v' tl -> v' <> new_var p) /\ well_sorted_partly_solved_part tl end.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)