The app invariant says that the argument in an `App` must not be unlifted. This gets in the way of rule matching on functions with unlifted arguments (#19313), and Simon PJ suggests that we may be better off without that invariant. There is an analogous invariant on lets (hence “let-app-invariant”). He suggests to keep the let-invariant. (And I suggest to henceforce call it the “let-lifted-invariant” for more clarity.) I’ll give it a shot and see what comes up.