proposition: Theorem rpo_mul_subst : forall A B: (list term), forall bb:nat, rpo_mul bb A B -> forall sigma, rpo_mul bb (map (apply_subst sigma) A) (map (apply_subst sigma) B).
proof: Proof. intros l' l bb0 Rmul sigma. inversion Rmul as [ a lg ls lc l0 k0 Pk Pl ls_lt_alg]; subst. apply (@List_mul bb0 (apply_subst sigma a) (map (apply_subst sigma) lg) (map (apply_subst sigma) ls) (map (apply_subst sigma) lc)). rewrite <- map_app; apply permut_map with equiv; trivial. intros b b' _ _ b_eq_b'; apply equiv_subst; trivial. rewrite <- map_app. refine (@permut_map term term term term equiv equiv (apply_subst sigma) _ _ (a :: lg ++ lc) _ _); trivial. intros b b' b_in_l _ b_eq_b'; apply equiv_subst; trivial. intros b b_mem_ls_sigma; destruct (mem_split_set _ _ equiv_bool_ok _ _ b_mem_ls_sigma) as [b' [ls1 [ls2 [b_eq_b' [H _]]]]]; simpl in b_eq_b'; simpl in H. assert (b'_in_ls_sigma : In b' (map (apply_subst sigma) ls)). rewrite H; apply in_or_app; right; left; trivial. rewrite in_map_iff in b'_in_ls_sigma. destruct b'_in_ls_sigma as [b'' [b''_sigma_eq_b' b''_in_ls]]. destruct (ls_lt_alg b'') as [a' [a'_mem_alg b''_lt_a']]. apply in_impl_mem; trivial. exact Eq. destruct (mem_split_set _ _ equiv_bool_ok _ _ a'_mem_alg) as [a'' [alg' [alg'' [a'_eq_a'' [H' _]]]]]; simpl in a'_eq_a''; simpl in H'. exists (apply_subst sigma a''); split; trivial. apply in_impl_mem. exact Eq. rewrite (in_map_iff (apply_subst sigma) (a :: lg)). exists a''; split; trivial. rewrite H'; apply in_or_app; right; left; trivial. rewrite (equiv_rpo_equiv_2 _ b_eq_b'). rewrite <- b''_sigma_eq_b'. apply rpo_subst. rewrite <- (equiv_rpo_equiv_1 _ a'_eq_a''); 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)