Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms