proposition: Lemma acc_one_step_list_2 : forall A R (l : list A), Acc (one_step_list R) l -> (forall t, In t l -> Acc R t).
proof: Proof. fix acc_one_step_list_2 4. intros A R l Acc_l t t_in_l; apply Acc_intro; intros s H. destruct (in_split t l t_in_l) as [l1 [l2 K]]. apply (acc_one_step_list_2 A R (l1 ++ s :: l2)). apply Acc_inv with l; trivial. subst l; clear Acc_l t_in_l; revert l1; fix Hone_step 1. intros [ | a1 l1]. left; assumption. right; apply Hone_step. apply in_or_app; right; left; apply eq_refl. Qed.
imports: Coq(Setoid Relations List Wellfounded)