proposition: Lemma Acc_inverse_image : forall x:A, Acc R (f x) -> Acc inverse_image x.
proof: Proof. intros; apply (Acc_lemma (f x)); trivial. Defined.
imports: Equations.Init Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties HoTT.Basics.Tactics