Judgement = Env "|-" Term ":" Type | Env "|-" Term | Term ":" Type | Term Term = Var | "fun" Var "->" Term | Term Term | "(" Term ")" Type = Var | Type "->" Type | "(" Type ")" Var = variable starting with a lower case letter | metavariable starting with an upper case letter Env = Var | Var ":" Type "," Env | "(" Env ")"