E) can be applied to the conclusions of u(Ap) and u(AQ).
E. if A' is also a TA1-deduction of F F-* M:T then A' _ A. ) 2B The subject-construction theorem 23 The following three lemmas will be needed in the next section. The first is a special case of the third but is stated separately because it is needed in the proof of the third. 2B4 First Substitution Lemma for Deductions Let F - M:T and let [y/x]F be the result of substituting y for a term-variable x in F. if either of the following holds: (i) y Subjects(F), (ii) y and x receive the same type in F, then [Y/x]r H2 ([Ylx]M) : T.
Thus the problem of deciding whether PQ is typable reduces to that of finding §I and §2 such that §I(p) §2(T). This suggests the next two definitions. ) of the pair (p, T), and we call (sI,§2) a pair of converging substitutions for (p, T). , p,,) and (t1...... n). Common instances of pairs of deductions are defined similarly. 1 Example A common instance of the pair (a->(b-*c), (a-+b)->a) is the type (where /3, y, b are any given types), and the corresponding converging substitutions are sl = fl/b, y/c), §2 = [(l3-'Y)la, Slb].
Basic Simple Type Theory by J. Roger Hindley