proposition: Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun y:{ y:A | R y x} => Fix_sub (proj1_sig y)).
proof: Proof. intro x; unfold Fix_sub. rewrite <- (Fix_F_eq ). apply F_ext; intros. apply Fix_F_inv. Qed.
imports: Coq.Init.Wf Coq.Program.Utils