proposition: Lemma acc_inv_im : forall A B (R1 : relation A) (R2 : relation B) (f : A -> B), (forall a1 a2, R1 a1 a2 -> R2 (f a1) (f a2)) -> forall a, Acc R2 (f a) -> Acc R1 a.
proof: Proof. intros A B R1 R2 f H a. set (b := f a) in *. assert (b_eq_fa := eq_refl b). unfold b at 2 in b_eq_fa; clearbody b. intro Acc_b; revert a b_eq_fa; induction Acc_b as [b Acc_b IH]. intros a b_eq_fa; apply Acc_intro; intros a' H'. apply IH with (f a'); trivial. subst b; apply H; trivial. Qed.
imports: Coq(Setoid Relations List Wellfounded)