Functional Programming, Formal Methods.
allowing a type to refer to its typed value, we have that, inside the definition of ind, when we apply n to P S Z, it returns P n, as expected, simply because the type of Nat specifies so. Without self types, we didn’t have a way to express such Nat type, for the mere reason there wasn’t a n in