fact: Fixpoint build_well_formed_matching_problem_list (lpb : list matching_problem) : (forall p, In p lpb -> well_formed_pb p) -> list well_formed_matching_problem := match lpb return (forall p, In p lpb -> well_formed_pb p) -> list well_formed_matching_problem with | nil => fun _ => nil | pb :: tl_lpb => fun proof => (W pb (proof pb (or_introl _ (eq_refl _)))) :: (build_well_formed_matching_problem_list tl_lpb (@tail_prop _ _ pb tl_lpb proof)) end.
imports: Coq(Arith List Wellfounded Wf_nat) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory ac matching dickson matching_well_formed matching_well_founded matching_sound matching_complete dickson)