∀ {m : Type u_1 → Type u_2} {α α_1 : Type u_1} {p₁ : (α → α_1) → Prop} {p₂ : α → Prop} [inst : Applicative m]
  (motive : (f : m (α → α_1)) → (x : m α) → SatisfiesM p₁ f → SatisfiesM p₂ x → Prop) (f : m (α → α_1)) (x : m α)
  (hf : SatisfiesM p₁ f) (hx : SatisfiesM p₂ x),
  (∀ (f : m { a // p₁ a }) (x : m { a // p₂ a }), motive (Subtype.val <$> f) (Subtype.val <$> x) ⋯ ⋯) → motive f x hf hx