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.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.Relation Equations.HoTT.WellFounded Equations.HoTT.DepElim Equations.HoTT.Constants HoTT(Basics.Tactics Spaces.Nat)