Comment by catnaroek

I'd like to know if the most scalable technique for reasoning about program data works: structural induction!

Is Eta strict or lazy?