no goals
α : Type u
m n o : ℕ
m' : Type ?u.15284
n' : Type ?u.15287
o' : Type ?u.15290
x : α
u : Fin n → α
y : α
⊢ y ∈ Set.range (vecCons x u) ↔ y ∈ {x} ∪ Set.range u
simp [Fin.exists_fin_succ, eq_comm]