proposition: Lemma term_acc_subst : forall R t sigma, Acc (one_step R) (apply_subst sigma t) -> Acc (one_step R) t.
proof: Proof. assert (H : forall R s, Acc (one_step R) s -> forall t sigma, s = (apply_subst sigma t) -> Acc (one_step R) t). intros R s Acc_s; induction Acc_s as [s Acc_s IH']; intros t sigma H. subst s. assert (IH : forall u tau, one_step R (apply_subst tau u) (apply_subst sigma t) -> Acc (one_step R) u). intros u tau H; apply (IH' _ H u tau); trivial. clear IH'. apply Acc_intro. intros u u_R_t; apply IH with sigma. apply one_step_apply_subst; trivial. intros R t sigma H'; apply H with (apply_subst sigma t) sigma; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)