proposition: Lemma nf_P_step_subterm: forall R P t, nf (P_step R P) t -> forall s, direct_subterm s t -> nf (P_step R P) s.
proof: Proof. intros R P 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 P_in_context; clear IH Hnf s_in_l; induction l' as [ | s' l']; simpl. left; trivial. right; apply IHl'. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)