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. constructor. Defined.
imports: Coq(Extraction CRelationClasses) Equations.Init Equations.CoreTactics Equations.Type.Logic Equations.Type.FunctionalExtensionality Equations.Type.Relation Equations.Type.Relation_Properties