feat(library/tactic): add beta-reduction tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/parser): simplified theorem definition using tactical proof

When using tactics for proving theorems, a common pattern is

     Theorem T : <proposition> := _.
          apply <tactic>.
          ...
          done.

This commit allows the user to write the simplified form:

     Theorem T : <proposition>.
          apply <tactic>.
          ...
          done.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(*): typo

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>