Tactics

Here we list all features we support at the moment.

1. scase: equivalent to SSReflect's case
2. scase_if: does case analysis on the first if statement
3. elim: equivalent to SSReflect's elim
4. move: Reduces goal to the weak head normal form
5. moveR: like move but only reduces [@ reducable] definitions
6. apply t in H: applies term t in hypothesis H, and moves the result on top the proof stack. H should not necessarily be the first argument of t, tactic will figure out which argument to instantiate automatically. It will also instantiate all other arguments of t which can be deduced from H
7. shave: Same as in SSReflect, it asserts a term of type ty (introducing a new goal for it), puts it on the proof stack, and runs intro_pats.
8. srw: SSReflect version of rw see rewrite patterns page.