proposition: Theorem wf_inverse_image : well_founded R -> well_founded inverse_image.
proof: Proof. red; intros; apply Acc_inverse_image; auto. Defined.
imports: Coq(Extraction CRelationClasses) Equations.Init Equations.CoreTactics Equations.Type.Logic Equations.Type.FunctionalExtensionality Equations.Type.Relation Equations.Type.Relation_Properties