proposition: Lemma rpo_mul_inclusion_permut0_right : forall rpo_infos l0 l1 l2 l3, permut0 equiv l0 l1 -> rpo_mul (bb rpo_infos) (l2++ l0) (l3 ++ l1) -> rpo_mul (bb rpo_infos) l2 l3.
proof: Proof. intros. inversion H0. assert (permut0 equiv (l2 ++ l1) (ls ++ lc)). apply permut0_trans with (l2 ++ l0). apply equiv_equiv. rewrite <- permut0_app1. apply permut0_sym. apply equiv_equiv. trivial. apply equiv_equiv. trivial. assert (rpo_mul (bb rpo_infos) (l2 ++ l1) (l3 ++ l1)). apply List_mul with a lg ls lc. trivial. trivial. trivial. apply rpo_mul_inclusion_right with l1. 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)