Function application as the elimination rule for function types