`whnf` doesn't unfold applications where the head is a declaration

The following definition bad should work but doesn't:

def foo.{} := fun x:Prop => Prop
def False := (A:Prop) -> A
def bad : foo.{} False := False```