I use Coq to verify properties of novel rewriting systems, as a basis for computation. These include all theorems in my recent book “Reflective Programs in Tree Calculus”. I would like to improve my use of tactics.