CoqIde: показать, что делает простая тактика

Question

Используя CoqIde, есть ли способ просмотреть шаги, предпринятые simpl? Я нахожу, что не понимаю, как он достиг своего результата довольно часто.

Пример:

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