refine ⟨⟨x,?_⟩,?_⟩
n : Nat
x : Fin n
⊢ ∃ n_1, get (fins n) n_1 = x
case refine_1
n : Nat
x : Fin n
⊢ ↑x < length (fins n)

case refine_2
n : Nat
x : Fin n
⊢ get (fins n) { val := ↑x, isLt := ?refine_1 } = x