proposition: Lemma trans_clos_stepr A (R : relation A) (x y z : A) : R y z -> trans_clos R x y -> trans_clos R x z.
proof: Proof. intros Hyz Hxy. exact (t_trans _ x y z Hxy (t_step _ _ _ Hyz)). Defined.
imports: Equations(Init Signature) Equations.CoreTactics Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec Equations.Type.Relation Equations.Type.FunctionalExtensionality Equations.Type.WellFounded Equations.Type.DepElim Equations.Type.Constants