proposition: Lemma weight_is_weight : forall lpb, forall proof : (forall p, In p lpb -> well_formed_pb p), map wfpb_weight (build_well_formed_matching_problem_list lpb proof) = map pb_weight lpb.
proof: Proof. induction lpb. intros; trivial. simpl; intro proof; rewrite IHlpb; trivial. Qed.
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)