Complete Types in an Extension of the System AF2

Samir Farkh, Karim Nour

In this paper, we extend the system AF2 in order to have the subject reduction for the $\beta \eta$-reduction. We prove that the types with positive quantifiers are complete for models tha…