One thing I'm coming to appreciate about #LiquidHaskell is that lazy execution simplifies the handling of code whose only purpose is to generate a needed type (like a lemma.) In #FStarLang these are explicitly "ghost" functions which don't appear in the generated code. In Haskell, if you don't use the value, it just doesn't get executed!