Comment by extrabajs

I don’t see the connection to dependent types. But anyway, is ‘redef’ part of your language? What type would you give it?