feat: allow `optParam` and `autoParam` in implicit binders

This PR allows default values and auto-param tactics on implicit binders, as in `{n : Nat := 5}` and `{h : i < n := by omega}`. Such a parameter is solved by unification like a regular implicit argument; the default value or tactic is used only if unification leaves it unassigned.

Previously this syntax was a parse error, and an `optParam`/`autoParam` annotation reaching an implicit binder by other means was silently ignored.