rw [this]
α : Type u_1
inst✝ : Finite α
n✝ n : ℕ
ih : {l | l.length = n}.Finite
this : {l | l.length = n + 1} = image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}
⊢ {l | l.length = n + 1}.Finite
α : Type u_1
inst✝ : Finite α
n✝ n : ℕ
ih : {l | l.length = n}.Finite
this : {l | l.length = n + 1} = image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}
⊢ (image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}).Finite