Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion

From MaRDI portal