proposition: Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y.
proof: Proof. induction 1 as [| x y]; auto with relations. intro; apply Acc_inv with y; assumption. Defined.
imports: Coq(Extraction CRelationClasses) Equations.Init Equations.CoreTactics Equations.Type.Logic Equations.Type.FunctionalExtensionality Equations.Type.Relation Equations.Type.Relation_Properties