Kőnig/weak Kőnig for List-based trees via Mathlib's exists_seq_forall_proj_of_forall_finite

To get a path through a prefix-closed T : Set (List α) with nodes at every level, instantiate Mathlib's exists_seq_forall_proj_of_forall_finite with α i := {σ // σ ∈ T ∧ σ.length = i} and π hij a := ⟨a.1.take i, ...⟩; π_trans is List.take_take + Nat.min_eq_left. For Finite (α i) with Bool entries inject into Fin i → Bool (needs Mathlib.Data.Fintype.Pi imported; List.Vector has no Finite instance without extra imports). For finitely branching ℕ-trees, hfin follows by Set.Finite.of_finite_image with b ↦ b.1.getD i 0 into {k | a ++ [k] ∈ T} plus the lemma σ.length = i+1 → σ = σ.take i ++ [σ.getD i 0] (from List.take_add_one). Read off the path as n ↦ (g (n+1)).1.getD n default and compare initial segments with List.ext_getElem?, case-splitting on e < n; working with getElem instead of getElem? runs into dependent-index rewrite failures.