{α : Type u_1} →
  (p : α → Prop) →
    (xs : List α) →
      (motive : Decidable (∃ x ∈ xs, p x) → Sort u_2) →
        (x : Decidable (∃ x ∈ xs, p x)) →
          ((h₂ : ∃ x ∈ xs, p x) → motive (isTrue h₂)) → ((h₂ : ¬∃ x ∈ xs, p x) → motive (isFalse h₂)) → motive x