Try alectryon as a way to generate readable proofs

[awalterschulze]

https://github.com/cpitclaudel/alectryon

The video gives a pretty great demo, but I can't find it now

Here is also a nice example https://alectryon-paper.github.io/bench/stdlib/theories/Lists/List.html

Seems we can add (* .unfold *) to force unfolding of the state in the generated document/webpage and we can use (* .none *) to not add lines to the generated document, see the induction example on https://alectryon-paper.github.io/

[paulcadman]

https://people.csail.mit.edu/cpitcla/links/2020-08-05-alectryon.pdf