proposition: Lemma nf_one_step_subterm: forall R t, nf (one_step R) t -> forall s, direct_subterm s t -> nf (one_step R) s.
proof: Proof. intros R t; pattern t; apply term_rec3; clear t. intros v _ s H; contradiction. simpl; intros f l IH Hnf s s_in_l u H. destruct (In_split _ _ s_in_l) as [l' [l'' H']]; subst. apply (Hnf (Term f (l' ++ u :: l''))). apply in_context; clear IH Hnf s_in_l; induction l' as [ | s' l']; simpl. apply head_step; trivial. apply tail_step; apply IHl'. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)