proposition: Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y.
proof: Proof. induction 1 as [| x y]; auto with Relations. intro; apply Acc_inv with y; assumption. Defined.
imports: Equations.Init Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties HoTT.Basics.Tactics