proposition: Lemma rpo_mul_inclusion_left : forall rpo_infos l1 l2 l3, rpo_mul (bb rpo_infos) (l1++ l2) (l1 ++ l3) -> rpo_mul (bb rpo_infos) l2 l3.
proof: Proof. induction l1. simpl. intros. trivial. intros. apply IHl1. assert (((a:: l1) ++ l2) = a :: (l1 ++ l2)). simpl. trivial. assert (((a :: l1) ++ l3) = a:: (l1 ++ l3)). simpl. trivial. rewrite H0 in H. rewrite H1 in H. apply rpo_mul_remove_equiv_aux1 with a a. reflexivity. 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)