On 11 April 2016 at 20:14, Andreas Abel <andreas.abel at ifi.lmu.de> wrote: > You could implement a tactic using Agda's new tactic language that does such > routine jobs for you. Where can one find out about that? Andy