{α : Type u_1} →
  {β : Type u_2} →
    {f : α → β} →
      {P : β → Prop} →
        (motive : { x // (P ∘ f) x } → Sort u_3) →
          (x : { x // (P ∘ f) x }) → ((x : α) → (h : (P ∘ f) x) → motive ⟨x, h⟩) → motive x