Agda.Compiler.UHC.Smashing