ext (_ | _) <;> simp [n.succ_ne_zero.symm]
case succ
α : Type u_1
inst✝ : Finite α
n✝ n : ℕ
ih : {l | l.length = n}.Finite
⊢ {l | l.length = n + 1} = image2 (fun x x_1 => x :: x_1) univ {l | l.length = n}
no goals