S = λx:Int. x + 1 S : Int → Int
twice = λf:Int → Int. λy : Int . f ( f ( y ) ) twice : ( Int → Int ) → Int → Int
S 0 = 1 ∈ Int
twice ( S ) = λx. S S x ∈ Int → Int
slide
:
Subtypes -- examples