proposition: Lemma inv_solved_part_init : forall t1 t2, Inv_solved_part (mk_pb nil ((t1, t2) :: nil)).
proof: Proof. intros t1 t2; unfold Inv_solved_part; simpl; trivial. Defined.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)