Comment by yababa_y

I love this walkthrough! It reproduces, in narrative form, the experience of interactive theorem proving. Great exploration of a niche detail.