proposition: Lemma one_step_subterm_subst : forall R s t sigma, refl_trans_clos (union _ (one_step R) (direct_subterm)) s t -> refl_trans_clos (union _ (one_step R) (direct_subterm)) (apply_subst sigma s) (apply_subst sigma t).
proof: Proof. intros R s t sigma [s' | s' t' H]. left. right; induction H as [t1 t2 [H | H] | t1 t2 t3 H1 H2]. do 2 left; apply one_step_apply_subst; trivial. destruct t2 as [v2 | f2 l2]. contradiction. simpl in H. left; right; simpl; rewrite in_map_iff; exists t1; split; trivial. apply trans_clos_is_trans with (apply_subst sigma t2); trivial. destruct H1 as [H1 | H1]. do 2 left; apply one_step_apply_subst; trivial. destruct t2 as [v2 | f2 l2]. contradiction. simpl in H1. left; right; simpl; rewrite in_map_iff; exists t1; split; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)