proposition: Lemma acc_one_step_list : forall A R (l : list A), (forall t, In t l -> Acc R t) <-> Acc (one_step_list R) l.
proof: Proof. intros A R l; split; intro H. apply acc_one_step_list_1; assumption. apply acc_one_step_list_2; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)