proposition: Remark Acc_lemma : forall y:B, Acc R y -> forall x:A, y = f x -> Acc Rof x.
proof: Proof. induction 1 as [y _ IHAcc]; intros x H. apply Acc_intro; intros y0 H1. apply (IHAcc (f y0)); try trivial. rewrite H; trivial. Qed.