+ <!-- tactics -->
+ <keyword>absurd</keyword>
+ <keyword>apply</keyword>
+ <keyword>applyP</keyword>
+ <keyword>assumption</keyword>
+ <keyword>autobatch</keyword>
+ <keyword>cases</keyword>
+ <keyword>clear</keyword>
+ <keyword>clearbody</keyword>
+ <keyword>change</keyword>
+ <keyword>compose</keyword>
+ <keyword>constructor</keyword>
+ <keyword>contradiction</keyword>
+ <keyword>cut</keyword>
+ <keyword>decompose</keyword>
+ <keyword>destruct</keyword>
+ <keyword>elim</keyword>
+ <keyword>elimType</keyword>
+ <keyword>exact</keyword>
+ <keyword>exists</keyword>
+ <keyword>fail</keyword>
+ <keyword>fold</keyword>
+ <keyword>fourier</keyword>
+ <keyword>fwd</keyword>
+ <keyword>generalize</keyword>
+ <keyword>id</keyword>
+ <keyword>intro</keyword>
+ <keyword>intros</keyword>
+ <keyword>inversion</keyword>
+ <keyword>lapply</keyword>
+ <keyword>linear</keyword>
+ <keyword>left</keyword>
+ <keyword>letin</keyword>
+ <keyword>normalize</keyword>
+ <keyword>reflexivity</keyword>
+ <keyword>replace</keyword>
+ <keyword>rewrite</keyword>
+ <keyword>ring</keyword>
+ <keyword>right</keyword>
+ <keyword>symmetry</keyword>
+ <keyword>simplify</keyword>
+ <keyword>split</keyword>
+ <keyword>to</keyword>
+ <keyword>transitivity</keyword>
+ <keyword>unfold</keyword>
+ <keyword>whd</keyword>
+ <keyword>assume</keyword>
+ <keyword>suppose</keyword>
+ <keyword>by</keyword>
+ <keyword>is</keyword>
+ <keyword>or</keyword>
+ <keyword>equivalent</keyword>
+ <keyword>equivalently</keyword>
+ <keyword>we</keyword>
+ <keyword>prove</keyword>
+ <keyword>proved</keyword>
+ <keyword>need</keyword>
+ <keyword>proceed</keyword>
+ <keyword>induction</keyword>
+ <keyword>inductive</keyword>
+ <keyword>case</keyword>
+ <keyword>base</keyword>
+ <keyword>let</keyword>
+ <keyword>such</keyword>
+ <keyword>that</keyword>
+ <keyword>by</keyword>
+ <keyword>have</keyword>
+ <keyword>and</keyword>
+ <keyword>the</keyword>
+ <keyword>thesis</keyword>
+ <keyword>becomes</keyword>
+ <keyword>hypothesis</keyword>
+ <keyword>know</keyword>
+ <keyword>case</keyword>
+ <keyword>obtain</keyword>
+ <keyword>conclude</keyword>
+ <keyword>done</keyword>
+ <keyword>rule</keyword>