The HOL Logic Extended with Quantification over Type Variables - Melham, T (Formal Methods in System Design, 1994)