user_manual: fixing semantics of :implicit annotation

user_manual.md

@@ -236,7 +236,7 @@ In contrast, the example below declares a predicate `=` where the type of the ar
 (define P ((x Int) (y Int)) (= x y))
 ```
 
-In general, a type argument can be made implicit if its value can be inferred from the type of later arguments.
+In general, an argument can be made implicit if its value can be inferred from the type of later arguments.
 
 We call `T` in the above definitions a _parameter_. The free parameters of the return type of an expression should be contained in at least one non-implicit argument. In particular, the following declaration is malformed, since the return type of `f` cannot be inferred from its arguments: