  We define a sound and complete proof system for affine beta-eta-retractions
in simple types built over many atoms, and we state simple necessary conditions
for arbitrary beta-eta-retractions in simple and polymorphic types.
