fact: Definition ac_elementary_solve_term_var_without_val_term pb f x list_of_terms l' list_of_equations : list matching_problem := map12_without_repetition T.eq_bool (fun t => match remove T.eq_bool t l' with | None => (None, None) | Some rmv => let l'_without_t := rmv in let t1' := build f list_of_terms in let t2' := build f l'_without_t in let new_pb := mk_pb (existential_vars pb) ((t1', t2') :: list_of_equations) ((x, t) :: (solved_part pb)) (partly_solved_part pb) in if le_gt_dec (length l') ((length list_of_terms) + 1) then (Some new_pb, None) else let y := fresh_var pb in let t1'' := build f (Var y :: list_of_terms) in let new_pb' := mk_pb (y :: existential_vars pb) ((t1'', t2') :: list_of_equations) (solved_part pb) ((x, mk_pst f y t) :: (partly_solved_part pb)) in (Some new_pb, Some new_pb') end) l'.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)