proposition: Lemma Fix_sub_rect (Q: forall x, P x -> Type) (inv: forall (x: A) (H: forall (y: A), R y x -> Q y (Fix_sub A R Rwf P f y)) (a: Acc R x), Q x (f (fun y: {y: A | R y x} => Fix_sub A R Rwf P f (proj1_sig y)))) : forall x, Q _ (Fix_sub A R Rwf P f x).
proof: Proof. Proof with auto. unfold Fix_sub. intros x. apply Fix_F_sub_rect. intros x0 H a. assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y))) as X0... set (q := inv x0 X0 a). clearbody q. rewrite <- (equiv_lowers (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y))) (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))... intros. apply eq_Fix_F_sub. Qed.
imports: Coq.Init.Wf Coq.Program.Utils