proposition: Lemma FB_nf_dec : forall R FB, (forall t s, one_step R s t <-> In s (FB t)) -> forall t, {nf (one_step R) t}+{~ nf (one_step R) t}.
proof: Proof. intros R FB red_dec t. case_eq (FB t). intro FBt ; left; unfold nf; intros s; rewrite (red_dec t s); rewrite FBt; contradiction. intros s l FBt; right; unfold nf; intro nf_t. apply (nf_t s); rewrite (red_dec t s); rewrite FBt; left; trivial. Defined.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)