proposition: Lemma Acc_clos_trans : 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 sets. apply Acc_inv with y; auto with sets. Defined.
imports: Relation_Definitions Relation_Operators