proposition: Lemma Acc_tc_ind : forall P : A->Prop, (forall x, (forall y, clos_trans R y x -> P y) -> P x) -> forall x, Acc R x -> P x.
proof: Proof. intros. eapply Acc_ind with (R := clos_trans R). clear x H0. intros. apply H. intros. apply H1. hyp. apply Acc_clos_trans. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil)