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