proposition: Lemma acc_trans : forall A (R : relation A) a, Acc R a -> Acc (trans_clos R) a.
proof: Proof. intros A R a Acc_R_a. induction Acc_R_a as [a Acc_R_a IH]. apply Acc_intro. intros b b_Rp_a; induction b_Rp_a. apply IH; trivial. apply Acc_inv with y. apply IHb_Rp_a; trivial. apply t_step; trivial. Defined.
imports: Coq(Setoid Relations List Wellfounded)