The HOL Logic Extended with Quantification over Type Variables - Melham, T (1994)