Deductive lambda calculus