coq - CoqIde：展示简单的策略在做什么

Question

使用 CoqIde，有没有办法查看simpl已采取的步骤？我发现我不明白它是如何经常取得结果的。

例子：

rev (rev (n :: l')) = n :: l'
-- apply simpl. 
rev (rev l' ++ [n]) = n :: l'