proposition: Lemma nf_dec_inner_dec : forall R, (forall t, {nf (one_step R) t}+{~ nf (one_step R) t}) -> forall t, {inner R t}+{~inner R t}.
proof: Proof. intros R nf_dec [v | f l]. left; intro s; simpl; contradiction. unfold inner; simpl; induction l as [ | t l]. left; intro s; simpl; contradiction. destruct (nf_dec t) as [nf_t | red_t]. destruct IHl as [nf_l | red_l]. left; intros s [s_eq_t | s_in_l]; [subst | apply nf_l]; trivial. right; intro nf_tl; apply red_l; intros s s_in_l; apply nf_tl; right; trivial. right; intro nf_tl; apply red_t; apply nf_tl; left; trivial. Defined.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)