Independence of the induction principle and the axiom of choice in the pure calculus of constructions
scientific article; zbMATH DE number 94467