L'interprétation du λ-calcul simplement typé est correcte dans toute ccc