Title: On Church's Lambda Delta Calculus
Author: Richard Statman 

Abstract:
   In 1941 Church [2] introduced the lambda-delta calculus in an
untyped context. The purpose of this note is to investigate 
Church's calculus in a simply typed setting and to establish
the fundemental properties of this calculus. Toward this end
we add to classical type theory a conditional d (definition
by cases functional) at all finite types A -> (A -> (B -> (B -> B))).
This functional (IF_THEN_ELSE_) is defined by the non-
equational condition
                /\xyuv. ( x=y => dxyuv = u  &  ~x=y => dxyuv = v ).