coq - Coqでの単純化中に関数を1回適用する方法は?

Question

私が理解していることから、Coq の関数呼び出しは不透明です。場合によっては、unfoldそれを適用してからfold、関数定義/本体をその名前に戻す必要があります。これはしばしば面倒です。私の質問は、関数呼び出しの特定のインスタンスを適用させる簡単な方法はありますか?

最小限の例として、リストのl場合、右追加[]が変更されないことを証明するにはl:

Theorem nil_right_app: forall {Y} (l: list Y), l ++ [] = l.
Proof.
  induction l. 
    reflexivity. 

これは次のとおりです。

1 subgoals
Y : Type
x : Y
l : list Y
IHl : l ++ [] = l
______________________________________(1/1)
(x :: l) ++ [] = x :: l

++ここで、 (ie )の定義を一度適用する必要があります(適用/拡張したくない目標にapp他の定義があるふりをします)。++現在、この 1 回限りのアプリケーションを実装する唯一の方法は、最初に展開++してから折りたたむことです。

    unfold app at 1. fold (app l []).

与える:

______________________________________(1/1)
x :: l ++ [] = x :: l

しかし、 で使用する用語の形を理解しなければならないので、これは不便foldです。Coqではなく、私が計算しました。私の質問は次のとおりです。

このワンタイム関数アプリケーションを同じ効果に実装する簡単な方法はありますか?