This allows for automatic declaration of fin_scope when in a function argument of type fin n. For example in a defined function f {n}: fin n → T, you can now do f 45 instead of f 45%fin (assuming the n can be deduced of course). This might be a breaking change in very weird circumstances, but it otherwise allows a more convenient use of the fin notations.