proposition: Lemma one_step_apply_subst : forall R t1 t2 sigma , one_step R t1 t2 -> one_step R (apply_subst sigma t1) (apply_subst sigma t2).
proof: Proof. intros R t; pattern t; apply term_rec3; clear t. intros x1 t2 sigma H; inversion_clear H as [ t1' t2' H'|]; inversion_clear H' as [ t1' t2' tau H'']; do 2 (rewrite <- subst_comp_is_subst_comp); auto. intros f1 l1 Hrec t2 sigma H; inversion_clear H as [ t1' t2' H'| f l1' l2 H'']. inversion_clear H' as [ t1' t2' tau H'']; do 2 (rewrite <- subst_comp_is_subst_comp); auto. simpl; apply in_context; generalize l2 H''; clear l2 H''; induction l1 as [ | a1 l1]. intros l2 H; inversion_clear H. intros l2' H; inversion_clear H as [ t1' a2 l H' | t' l1' l2 H']. simpl; apply head_step; apply Hrec; trivial; left; trivial. simpl; apply tail_step; apply IHl1; trivial; intros; apply Hrec; trivial; right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)