∀ {α : Type u_3} {β : Type u_1} {m : α → Filter β} (G : (i : α) → (m i).Realizer) (x : Set β) (σ : Type u_2)
  (F : CFilter (Set α) σ) (motive : x ∈ {a | ∃ a_1 b, ∀ (i : α) (i_1 : i ∈ F.f a_1), (G i).F.f (b i i_1) ⊆ a} → Prop)
  (x_1 : x ∈ {a | ∃ a_1 b, ∀ (i : α) (i_1 : i ∈ F.f a_1), (G i).F.f (b i i_1) ⊆ a}),
  (∀ (s : σ) (f : (i : α) → i ∈ F.f s → (G i).σ) (h : ∀ (i : α) (i_1 : i ∈ F.f s), (G i).F.f (f i i_1) ⊆ x), motive ⋯) →
    motive x_1