An outsider's impression: "type assumption" for G goes well with "type assertion" for G |- M has type tau. (These from Mitch's and Andy's messages respectively.) Vaughan Pratt