proposition: Lemma clos_rt_idempotent : subrelation (R*)* R*.
proof: Proof. red. induction 1; auto with Relations. intros. apply rt_trans with y; auto with Relations. Defined.
imports: Equations.Init Equations.HoTT.Logic Equations.HoTT.Relation