proposition: Lemma rpo_subst : forall t s, rpo s t -> forall sigma, rpo (apply_subst sigma s) (apply_subst sigma t).
proof: Proof. intro t; pattern t; apply term_rec3; clear t. intros v s H; inversion H. intros f l IHl s; simpl; pattern s; apply term_rec3; clear s. intros v R; inversion R as [ f' l' s' t In_t_l R' H1 H2 | | | ]; subst; intro sigma; simpl; apply Subterm with (apply_subst sigma t). apply in_in_map; trivial. inversion R' as [ s' R'' | s' t' R'' ]; subst; simpl; [ apply Eq| apply Lt; refine (IHl _ In_t_l _ R'' sigma) ]. intros g k IHl' R sigma; inversion R as [ f' l' s' t In_t_l R' H1 H2 | f' g' l' l'' R' R'' H1 H2 | g' l' k' f_lex Rlex R' H2 H3 | g' l' k' f_mul Rmul R' H2 ]; subst. apply Subterm with (apply_subst sigma t). apply in_in_map; trivial. inversion R' as [ s' R'' | s' t' R'' ]; subst; [ apply Eq | apply Lt; apply IHl; trivial ]. simpl; apply Top_gt; trivial. intros s' In_s'; elim (in_map_in _ s' _ In_s'); intros s [H1 H2]; subst. apply IHl'; trivial; apply R''; trivial. simpl; apply Top_eq_lex; trivial. generalize l Rlex IHl; clear l R Rlex R' IHl IHl'; induction k as [ | s' k ]; intros l Rlex IHl; inversion Rlex; subst; simpl. apply List_gt; [ apply IHl; trivial; left | do 2 (rewrite length_map) ]; trivial. apply List_eq; apply IHk; trivial; intros; apply IHl; trivial; right; trivial. intros s' In_s'; elim (in_map_in _ s' _ In_s'); intros s [In_s H1]; subst; apply IHl'; trivial; apply rpo_trans with (Term f k); trivial; apply Subterm with s; trivial; apply Eq. simpl; apply Top_eq_mul; trivial. inversion Rmul as [ a lg ls lc l0 k0 Pk Pl H]; subst. apply (List_mul (apply_subst sigma a) (map (apply_subst sigma) lg) (map (apply_subst sigma) ls) (map (apply_subst sigma) lc)). rewrite <- map_app; apply list_permut_map; trivial. rewrite <- map_app; generalize (list_permut_map (apply_subst sigma) Pl); simpl; trivial. intros b' In_b'; elim (in_map_in _ b' _ In_b'); intros b [In_b H1]; subst; elim (H b In_b); intros a' [ In_a' H1 ]; exists (apply_subst sigma a'); split. generalize (in_in_map (apply_subst sigma) _ _ In_a'); simpl; trivial. apply IHl; trivial; apply in_permut_in with (a :: lg ++ lc). elim In_a'; clear In_a'; intro In_a'; subst. left; trivial. right; apply in_or_app; left; trivial. apply list_permut_sym; trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term