J'avoue mal connaître la correspondance de CurryHoward, mais sinon, côté propositionnel, comme tu le sais bien, {>} n'est pas un système complet de connecteur, il faut au moins en plus le faux (qui donne la négation : non(p) eq (p > Faux) ). Bref il y a til dans la <url> une particularité qui ferait que seule l'implication serait nécessaire au niveau propositionnel ?