exact ⟨.refl⟩
case case3
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi : first ≤ i
ij : i ≤ j
jn : ¬first < i
⊢ Nonempty (permuted n (↑first) (↑j) arr arr)
no goals