Completude d'un systeme formel pour prouver l'equivalence de certains schemas recursifs monadiques