proposition: Remark Acc_lemma : forall y : B, Acc R y -> forall x : A, y = f x -> Acc inverse_image x.
proof: Proof. induction 1 as [y _ IHAcc]; intros x H. apply Acc_intro; intros y0 H1. apply (IHAcc (f y0)); try trivial. apply id_sym in H. destruct H; trivial. constructor. Defined.
imports: Coq(Extraction CRelationClasses) Equations.Init Equations.CoreTactics Equations.Type.Logic Equations.Type.FunctionalExtensionality Equations.Type.Relation Equations.Type.Relation_Properties