Comment by yorwba

The promised next post is here: http://languagengine.co/blog/bidirectional-proof-refinement/