Without cumulativity, we do not have problems with Eta at whnf anymore.
When we had cumulativity, we could not not simply reduce
(fun x : A, f x) ==> f
This step is correct only if domain(f) was definitionally equal to f.
Here is a problematic example for systems with cumulativity
Given, f : Type.{2} -> Bool
(fun x : Type.{1}, f x)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
