proposition: Lemma Acc_trans_clos : forall x:A, Acc R x -> Acc trans_clos x.
proof: Proof. induction 1 as [x0 _ H1]. apply Acc_intro. intros y H2. induction H2; auto with Relations. apply Acc_inv with y; auto with Relations. Defined.
imports: Equations.Init Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties HoTT.Basics.Tactics