proposition: Lemma rpo_mul_dickson: forall bb l l', rpo_mul_rest bb l l' -> clos_trans (list term) (rpo_mul_step_rest bb) l l'.
proof: Proof. intros. assert (H1:= (rpo_mul_rest_trans_clos)). assert (H2:= H1 bb0). unfold inclusion in H2. assert (H2':= H2 l l'). assert ( clos_trans (list term) (rpo_mul_step_rest bb0) l l'). apply H2'; trivial. trivial. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)