Subformula linking for intuitionistic logic with application to type theory
scientific article; zbMATH DE number 7437080