Consider the simply-typed lambda calculus with sum-type constructors, and let Set be the standard set-theoretic model of this calculus over an infinite base set. We present a proof system for the calculus (which involves a rule for reasoning by cases) and prove it to be a complete axiomatization of the equational theory of Set. We also develop some results concerning the syntactic properties of the calculus and an interpretation in Set of the equational theory (in the language of the classical simply-typed calculus) of the full function hierarchy over one infinite and one finite base set.

We consider the following problem in proving observational congruences in functional languages: given a call-by-name language based on the simply-typed λ-calculus with algebraic operations axiomatized by algebraic equations E, is the set of observational congruences between terms exactly those provable from (β), (η), and E? We find conditions for determining whether βηE-equational reasoning is complete for proving the observational congruences between such terms. We demonstrate the power and generality of the theorems by presenting a number of easy corollaries for particular algebras.