proposition: Lemma incl_trans_clos : inclusion R trans_clos.
proof: Proof. red; auto with Relations. Defined.
imports: Equations.Init Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties HoTT.Basics.Tactics