<keyword>ncoinductive</keyword>
<keyword>nlet</keyword>
<keyword>nlemma</keyword>
+ <keyword>nremark</keyword>
<keyword>naxiom</keyword>
<!-- tactics -->
<!-- ntactics -->
<keyword>napply</keyword>
+ <keyword>napplyS</keyword>
<keyword>ncases</keyword>
<keyword>nletin</keyword>
<keyword>nauto</keyword>
<keyword>nchange</keyword>
<keyword>nrewrite</keyword>
<keyword>ncut</keyword>
+ <keyword>ninversion</keyword>
<keyword>nlapply</keyword>
<keyword>ndestruct</keyword>