proposition: Lemma clos_rt_t : forall x y z, clos_refl_trans R x y -> trans_clos R y z -> trans_clos R x z.
proof: Proof. induction 1 as [b d H1|b|a b d H1 H2 IH1 IH2]; auto. intro H. apply t_trans with (y:=d); auto. constructor. auto. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation