`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```

added Kernel label

assigned to @belazy

created branch 75-whnf-doesn-t-unfold-applications-where-the-head-is-a-declaration to address this issue

mentioned in merge request !57 (merged)

closed with merge request !57 (merged)

changed the incident status to Resolved by closing the incident

mentioned in commit 30fa4424