∀ {α : Type u_1} {inst : DecidableEq α} [inst_1 : DecidableEq α] {s : Finset α} (f : α → Type u_3) {a : α}
  (x x_1 : f a × ((i : α) → i ∈ s → f i)),
  x = x_1 → ∀ (i : α) (a_1 : i ∈ insert a s), Finset.prodPiInsert f x i a_1 = Finset.prodPiInsert f x_1 i ⋯