Henglein, F.H. (1990). A lower bound for full polymorphic type inference: Girard-Reynolds Typability is DEXPTIME-hard. (RUU-CS90-14 ). Utrecht. Henglein, F.H. (1989). Fast left-linear semi-unification. (RUU-CS89-33 ). Utrecht.