We present here a strongly normalizable extension of second order functional arithmetics (AF2) with subtyping, that allows to program with recursive types in the pure lambda-calculus (i.e., without constant). It assigns types to the Scott encoding of algebraic datatypes and to the recursor on those types. Thus, it answers the open question of finding a strongly normalizing type system which allows to program on Scott numerals. One of the key features of the system is to have no more typing rules than AF2. The new rules are only subtyping rules. The first-order layer is used to prove the correction of extracted programs. It is also worth noticing that in this system union type (both finite and infinite) are definable and still the system enjoys subject-reduction.