fact: Definition init_pb t1 t2 := mk_pb nil ((t1,t2) :: nil) nil nil.
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)