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: Equations.Init Equations.HoTT.Logic Equations.HoTT.Relation