proposition: Lemma Acc_trans_clos : forall x:A, Acc R x -> Acc trans_clos x.
proof: Proof. induction 1 as [x0 _ H1]. apply Acc_intro. intros y H2. induction H2; auto with relations. apply Acc_inv with y; auto with relations. Defined.
imports: Coq(Extraction CRelationClasses) Equations.Init Equations.CoreTactics Equations.Type.Logic Equations.Type.FunctionalExtensionality Equations.Type.Relation Equations.Type.Relation_Properties