Show and tell: small reaching definitions analysis for Imp

Stream: general

[ohhaimark]

Here is the code: https://github.com/badly-drawn-wizards/impdf/blob/master/Impdf.lean
My aim would be to eventually show it sound wrt the small step semantics. I'm doing this as I am reading through Principals of Program Analysis.
I hestitate to put this in the program verification channel as I have yet to do any verification :grinning_face_with_smiling_eyes: .