proposition: Lemma acc_one_step_list_1 : forall A R (l : list A), (forall t, In t l -> Acc R t) -> Acc (one_step_list R) l.
proof: Proof. fix acc_one_step_list_1 3. intros A R l; case l; clear l. intros _; apply Acc_intro; intros l' H; inversion H. intros a l Acc_l. assert (Acc_al : Acc (product_o R (one_step_list R)) (a,l)). apply acc_and. apply Acc_l; left; trivial. apply acc_one_step_list_1; intros; apply Acc_l; right; assumption. replace (a :: l) with ((fst (a,l) :: (snd (a,l)))); trivial. clear acc_one_step_list_1 Acc_l. generalize (a,l) Acc_al; clear a l Acc_al; intros al Acc_al; induction Acc_al as [[a l] Acc_al IH]; apply Acc_intro. intros [ | a' l'] H; inversion H; clear H; subst. apply (IH (a',l)). apply CaseA; trivial. apply (IH (a,l')). apply CaseB; trivial. Qed.
imports: Coq(Setoid Relations List Wellfounded)