Tactic tracing

[isovector]

This PR implements tactic tracing; eg for foldr it produces this trace:

auto
`- intros {f_b, b, l_a}
   `- destruct(auto)
      `- destruct l_a
         +- match [] {}
         |  `- assume b
         `- match : {a, l_a4}
            `- apply' f_b
               +- assume a
               `- recursion
                  `- apply' myfoldr
                     +- assume f_b
                     +- assume b
                     `- assume l_a4

Fixes #25