<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>