¿El sistema F con pares tiene fuertes propiedades de normalización y reducción de sujeto?

Es fácil ver en muchos libros de texto las pruebas de reducción de materia y fuerte normalización para el Sistema F, también, a veces hay definiciones de Sistema F con pares, donde (t, r) es un término, no solo una codificación. La pregunta es, ¿cuál sería la referencia para este sistema?

El tratamiento de los pares dados por la codificación, como el de Pruebas y Tipos , no es lo que generalmente desea, ya que no son "pares sobreyectivos", es decir, no hay una regla eta. Llamemos pares surjectivos, productos.

Se da una extensión del sistema F con productos y unidades en: Di Cosmo, 1995, Isomorfismos de tipos: desde cálculo lambda hasta recuperación de información y diseño de lenguaje , Birkhauser: Basilea.

Puede agregar tipos inductivos arbitrarios (positivos) al sistema F y mostrar que el sistema con los eliminadores apropiados es SN. Esto se trata en la tesis de Mendler aquí .