hlevel.hoq does not check anymore

[np]

hlevel.hoq:42:25: 
    Expected type: x = y
    Actual type:   x.proj1 , x.proj2 = y.proj1 , y.proj2
    Term: path (\i -> p @ i , path-over (\i' -> B (p @ i')) (x.proj2) (y.proj2) q @ i)

Eta on records seems to be at cause here.