proposition: Lemma accR2 : forall A (R : relation A) a, Acc R a <-> Acc (compose_rel R R) a.
proof: Proof. intros A R a; split. intro Acc_a; apply Acc_incl with (trans_clos R). intros x z H; inversion H as [x' y z' H1 H2]; clear H; subst; apply t_trans with y; trivial. apply t_step; trivial. apply acc_trans; trivial. intros Acc_a; induction Acc_a as [a Acc_a IH]. apply Acc_intro; intros b H; apply Acc_intro; intros c H'. apply IH; apply Comp with b; trivial. Qed.
imports: Coq(Setoid Relations List Wellfounded)