proposition: Lemma acc_nf : forall A (R : relation A) FB, (forall t s, In s (FB t) <-> R s t) -> forall t, Acc R t -> { s : A | nf R s /\ (s = t \/ trans_clos R s t)}.
proof: Proof. intros A R FB red_dec t Acc_t; induction Acc_t as [t Acc_t IH]. case_eq (FB t). intro H; exists t; split. intros s H'; rewrite <- red_dec in H'; rewrite H in H'; trivial. left; trivial. intros a l H; destruct (IH a) as [a' [nf_a' H']]. rewrite <- red_dec; rewrite H; left; trivial. exists a'; split; trivial. destruct H' as [a'_eq_a | H']. subst; right; apply t_step; rewrite <- red_dec; rewrite H; left; trivial. right; apply trans_clos_is_trans with a; trivial. apply t_step; rewrite <- red_dec; rewrite H; left; trivial. Defined.
imports: Coq(Setoid Relations List Wellfounded)