Title: A proof generating system for higher-order logic