Vollständigkeit und Schnittelimination in der intuitionistischen Typenlogik. Horst Osswald (1972) Manuscripta mathematica