∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} {s : Finset ι}
  [inst_1 : DecidablePred Subgroup.FiniteIndex] (D : Subgroup G)
  (t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i))
  (f : (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1}) → G)
  (K : (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1}) → Subgroup G) ⦃i : ι⦄ ⦃x : G⦄,
  let κ := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1});
  ∀ (motive : (∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D) → Prop) (x_1 : ∃ k, ↑k.fst = i ∧ K k = D ∧ x ∈ f k • ↑D),
    (∀ (k₁ : κ) (hik₁ : ↑k₁.fst = i) (hk₁ : K k₁ = D) (hxk₁ : x ∈ f k₁ • ↑D), motive ⋯) → motive x_1