forall f : nat -> Type, f x where x : nat := 1
     : Type