proposition: Lemma acc_inv_im3 : forall A B (R1 : relation A) (R2 : relation B) (f : A -> B), forall a, (forall a1 a2, R1 a2 a1 -> refl_trans_clos R1 a1 a -> R2 (f a2) (f a1)) -> Acc R2 (f a) -> Acc R1 a.
proof: Proof. intros A B R1 R2 f a Hinv Acc_b. set (b := f a) in *. assert (b_eq_fa := eq_refl b). unfold b at 2 in b_eq_fa; clearbody b. revert a b_eq_fa Hinv; induction Acc_b as [b Acc_b IH]. intros a b_eq_fa Hinv. apply Acc_intro; intros a2 H2. apply IH with (f a2); trivial. subst b; apply Hinv; trivial. left. revert Hinv H2; clear; intros Hinv H2. intros b1 b2 K2 K1. apply Hinv; trivial. inversion K1 as [b | b' a' K1']. right; left; assumption. right; apply trans_clos_is_trans with a2; trivial. left; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)