Literate Theorem Proving with Org (and Proof General) | Dark Hacker News