∀(x : Bool) → ∀(x : Natural) → { x : Natural }