Surely Coq can fill in the wholes, but it is completely abstract; it doesn&#x27;t use concrete examples to do this, and anyways, you really have to understand what it is doing.<p>The point of this kind of work is that it augments your thinking by allowing you to visualize and manipulate your concrete example. Before, you&#x27;d just have pen and paper for that, with no assistance from the computer at all. The whole formal kick really comes after you have enough intuition about the problem, this comes before that and aides in the intuition accumulation process.