proposition: Lemma Fix_F_sub_rect (Q: forall x, P x -> Type) (inv: forall x: A, (forall (y: A) (H: R y x) (a: Acc R y), Q y (Fix_F_sub A R P f y a)) -> forall (a: Acc R x), Q x (f (fun y: {y: A | R y x} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))) : forall x a, Q _ (Fix_F_sub A R P f x a).
proof: Proof. Proof with auto. set (R' := fun (x: A) => forall a, Q _ (Fix_F_sub A R P f x a)). cut (forall x, R' x)... apply (well_founded_induction_type Rwf). subst R'. simpl. intros. rewrite F_unfold... Qed.
imports: Coq.Init.Wf Coq.Program.Utils