∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} {f : (i : Fin (n + 1)) → α i} {s : (i : Fin (n + 1)) → Finset (α i)},
  f ∈ Fintype.piFinset s ↔ f (Fin.last n) ∈ s (Fin.last n) ∧ Fin.init f ∈ Fintype.piFinset (Fin.init s)