proposition: Theorem rpo_mul_rest_trans: forall bb l1 l2 l3, well_founded (prec Prec) -> rpo_mul_rest bb l1 l2 -> rpo_mul_rest bb l2 l3 -> rpo_mul_rest bb l1 l3.
proof: Proof. intros. assert (H2:= @rpo_mul_trans bb0 l1 l2 l3). assert (H3:=wf_rpo). assert (well_founded (rpo bb0)). apply H3. trivial. apply Rpo_mul_rest. intros. unfold well_founded in H4. apply H4. intros. unfold well_founded in H4. apply H4. apply H2. destruct H0; trivial. destruct H1; 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)