It is easy to look in a lot of textbooks the proofs of subject reduction and strong normalisation for System F, also, sometimes there are definitions of System F with pairs, where (t,r) is a term, not only an encoding. The question is, what would be the reference for this system?
Does the System F with pairs have the strong normalisation and subject reduction properties?
reference request;lo.logic;type theory;lambda calculus;polymorphism
The treatment of pairs given by encoding, such as that in Proofs and Types, isn't what you usually want since they aren't surjective pairs, i.e., there is no eta rule.  Let's call surjective pairs, products.An extension of system F with products and unit is given in: Di Cosmo, 1995,  Isomorphisms of types: from lambda-calculus to information retrieval and language design,  Birkhauser: Basel.