proposition: Lemma eq_Fix_F_sub x (a a': Acc R x): Fix_F_sub A R P f x a = Fix_F_sub A R P f x a'.
proof: Proof. revert a'. pattern x, (Fix_F_sub A R P f x a). apply Fix_F_sub_rect. intros ? H **. rewrite F_unfold. apply equiv_lowers. intros. apply H. assumption. Qed.
imports: Coq.Init.Wf Coq.Program.Utils