Title: Extensional Constructs in Intensional Type Theory
Subjects: Automatic theorem proving, Functional programming (computer science), Logic, symbolic and mathematical