When comparing the types of the existential T and its definition T' the ordering was wrong: it was T <= T' but it should be the other way around (as in the paper)