Verify the well-scopedness bugfix in Exitify
Verify the well-scopedness bugfix in Exitify

This completes the Well-Scopedness proof for Exitify, i.e. all Admitted
lemmas and Axioms are (I believe) about functions outside the `Exitify` module, i.e.
`WellScoped` and `VarSet` etc.

antalsz/hs-to-coq,antalsz/hs-to-coq