recursion - Coqで再帰関数を一度だけ展開する方法

Question

all_zero以下は、自然数のリストのすべてのメンバーがゼロかどうかをチェックする再帰関数です。

Require Import Lists.List.
Require Import Basics.

Fixpoint all_zero ( l : list nat ) : bool :=
  match l with
  | nil => true
  | n :: l' => andb ( beq_nat n 0 ) ( all_zero l' )
  end.

さて、次の目標があったとします。

true = all_zero (n :: l')

unfoldそして、私はそれを変換するために戦術を使用したかったのです

true = andb ( beq_nat n 0 ) ( all_zero l' )

unfold all_zero残念ながら、この戦術は のすべてのインスタンスを熱心に見つけて置換するため、簡単な方法では実行できません。これにall_zeroは、一度展開されたフォームのものも含まれます。これを回避し、再帰関数を一度だけ展開する方法はありますか?

とアドホックな同等性を証明することで同じ結果が得られることはわかっていますassert (...) as Xが、効率的ではありません。のような簡単な方法があれば教えていただきたいunfoldです。