∀(T : Type) → ∀(x : T) → Natural