1
Goal
The aim of this plugin is to make Jack's proof obligations proovable with Coq.