From Λ(Lin), one obtains Λ(LP), the terms in Curry-Howard correspondence with LP derivations, by adding one extra restriction, reflecting the requirement that sequent antecedents must be non-empty: every subterm contains at least one free variable. The derivations of LP are now read as judgements of a type inference system for Λ(LP).  Derivations are given in the natural deduction style, with elimination and introduction rules for the linear implication →. Judgements then are sequents of the form Γ ⊢ M : B.  Γ is a non-empty multiset of typing declarations x1 : A1, …, xn : An; the Ai and B are linear implicative types, and M is a Λ(LP) term of type B built out of the xi of type Ai. Axiom sequents are of the form x : A ⊢ x : A. Elimination and Introduction rules for the linear implication are given below. In the Introduction rule, x ∉ dom(Γ); in the Elimination rule dom(Γ) ∩ dom(Δ) = ∅.