Make reduce tactic identify shorter paths

[Russoul]

Example:

For function

let f : ℕ → ℕ → ℕ
    f ≔ ...

given an expression f 1 2
reduce ☐
should be interpreted the same way as
reduce ☐ _ _