no goals
α : Type u
m n o : ℕ
m' : Type ?u.21814
n' : Type ?u.21817
o' : Type ?u.21820
x y : α
u : Fin 0 → α
⊢ Set.range (vecCons x (vecCons y u)) = {x, y}
rw [range_cons, range_cons_empty, Set.singleton_union]