Representing inductively defined sets by wellorderings in Martin-Löf's type theory
scientific article; zbMATH DE number 1179140