λ(x : { a : {} }) → 0