fact: Definition o_lpb lwfpb1 lwfpb2 := (NatMul.multiset_extension_step lt) (map wfpb_weight lwfpb1) (map wfpb_weight lwfpb2).
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)