coq - Coq フィックスポイントを文字通り展開する方法

Question

定義を展開して、Fixpoint定義の本体を取得しようとしていました。しかし、Coq は定義の本体を文字どおりには提供しません。(fix ...)代わりに、それは私が利用できない で始まる何かを私に与えています。

たとえば、Coq.Init.Wfから以下を証明する場合

Lemma Fix_F_eq :
  forall (x:A) (r:Acc x),
  F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r.
  Proof. intros.

状態は次のとおりです。

...
______________________________________(1/1)
F x
  (fun (y : A) (p : R y x) =>
   Fix_F y (Acc_inv x r y p)) = 
Fix_F x r

さて、Fix_FRHS では、LHS とまったく同じように定義されました。

Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
  F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)).

私はそれを平等にしようとしましtrivialた:

unfold Fix_F at 2.

それでも、(fix Fix_F ... )RHS のようなものが得られたので、これ以上先に進むことはできません。

______________________________________(1/1)
F x
  (fun (y : A) (p : R y x) =>
   Fix_F y (Acc_inv x r y p)) =
(fix
 Fix_F (x0 : A) (r0 : Acc x0) {struct r0} :
   P x0 :=
   F x0
     (fun (y : A) (p : R y x0) =>
      Fix_F y (Acc_inv x0 r0 y p))) x r

質問は：

上記Fixpointを関数本体に展開する方法はありますか?

注: この例を証明するための回避策があることは知っています。

Proof. intros. destruct r. simpl. trivial. 
  Defined.

しかし、それが有効であれば、私はunfold-ing アプローチにもっと興味があります。