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 sets. intro; apply Acc_inv with y; assumption. Qed.
imports: Relation_Definitions Relation_Operators