proposition: Lemma rpo_mul_inclusion_right : forall rpo_infos l1 l2 l3, rpo_mul (bb rpo_infos) (l2++ l1) (l3 ++ l1) -> rpo_mul (bb rpo_infos) l2 l3.
proof: Proof. induction l1. intros. rewrite <- app_nil_end in H. rewrite <- app_nil_end in H. trivial. intros. apply IHl1. assert (rpo_mul (bb rpo_infos) (a:: (l2 ++ l1)) (a :: (l3 ++ l1))). inversion H. apply List_mul with a0 lg ls lc. assert (permut0 equiv (a :: l2 ++ l1) (l2 ++ a :: l1)). rewrite <- permut0_cons_inside. apply permut0_refl. auto with typeclass_instances. auto with typeclass_instances. reflexivity. apply permut0_trans with (l2 ++ a :: l1). auto with typeclass_instances. trivial. trivial. assert (permut0 equiv (a :: l3 ++ l1) (l3 ++ a :: l1)). rewrite <- permut0_cons_inside. apply permut0_refl. auto with typeclass_instances. auto with typeclass_instances. reflexivity. apply permut0_trans with (l3 ++ a :: l1). auto with typeclass_instances. trivial. trivial. trivial. 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)