proposition: Lemma clos_rt_clos_rst : subrelation (clos_refl_trans R) (clos_refl_sym_trans R).
proof: Proof. red. induction 1; auto with relations. apply rst_trans with y; auto with relations. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation