Application partielle
Soit Efoo l'environnement de définition de F2.
On peut appliquer F2 à une valeur x0 de type sx.
C'est une application partielle, le résultat en est une autre
fermeture :
Fx0= «y:-> E(x,y),ë(x=x0)<|Efooû»
qui a pour type sy ® sE
-
F1 et F2 n'ont pas le même type,
- On évalue F2 en liant x et y en même temps,
- F1 et F2 ne sont pas équivalentes.