proposition: Lemma dec_nf : forall A (R : relation A) FB, (forall t s, In s (FB t) <-> R s t) -> forall t, {nf R t}+{~nf R t}.
proof: Proof. intros A R FB red_dec t. case_eq (FB t). intro H; left; unfold nf; intros s H'; rewrite <- red_dec in H'; rewrite H in H'; contradiction. intros a l H. right; intro H'; apply H' with a. rewrite <- red_dec; rewrite H; left; trivial. Defined.
imports: Coq(Setoid Relations List Wellfounded)