Supplemental VM image and sources of the ICFP'22 paper "'do' Unchained: Embracing Local Imperativity in a Purely Functional Language" This supplement consists of a Lean 4 package containing translation rules and example proofs of equivalence as described in the paper. Each extension is declared in a separate `.lean` file in the `Do` directory. `Do/Formal.lean` contains the formalization of the equivalence proof written in a literate style explaining more details not mentioned in the paper. Each Lean file comes with a corresponding `.html` file rendered using Alectryon that allows for exploring the file including type and goal information in any browser without installing Lean. The directory `gh-survey` contains simple scripts for aggregating the use of extended `do` notation from Lean projects on GitHub.