proposition: Lemma clos_rt_clos_rst : inclusion (clos_refl_trans R) (clos_refl_sym_trans R).
proof: Proof. red. induction 1 as [x y H|x|x y z H IH H0 IH0]; auto with sets. apply rst_trans with y; auto with sets. Qed.
imports: Relation_Definitions Relation_Operators