Fully implement do unchained paper in Lean4

[FrederickPu]

The do unchained paper does not contain a full reference implementation of the hygienic macro system based version of lean4's do notation.

Goal is to create a fully implemented reference implementation so that progress that we can begin prototyping on adding dependently typed mutable vars to lean's do notation.

Another [stretch] would be to implement the same system again using lean's parser and elaborator system and explore what verification approaches can be used to show equivalence between the two systems.

That is do' hygenic is equivalent to do' parser elaborator

See the following paper:
https://dl.acm.org/doi/pdf/10.1145/3547640