3.2类型和项 ·定型规则 M:o (add var) T,x:t M:o T,x:o M:t (>Intro） (入x:o.)：σ→E TM:o→TN:o (→Elim) T MN:t ·定型断言的证明叫做定型推导3.2 类型和项 • 定型规则 (add var) (→ Intro) (→ Elim) • 定型断言的证明叫做定型推导  M : , x : M :  M : →  N :  MN : , x : M :  ( x : . M) :  →