proposition: Lemma one_step_Rwf : forall s t, one_step R t s -> Rwf t s.
proof: Proof. intros s t H; apply Ren. unfold collapse_subst. replace (T1.apply_subst (map (fun v : T1.variable => (v, T1.Var (inject 0))) (T1.var_list t)) t) with (T1.apply_subst (map (fun v : T1.variable => (v, T1.Var (inject 0))) (T1.var_list s)) t). apply one_step_apply_subst; trivial. rewrite <- subst_eq_vars; intros v v_in_t. assert (v_in_s : In v (var_list s)). apply R_reg_one_step with t; trivial. simpl. rewrite find_col; trivial. rewrite find_col; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)