[tel]

Sorry, not referring to the whole post wrt Agda, just the vision of interactivity that proof search and tactics give you.