def List.findExisting {α : Type} (p : α → Bool) (l : List α) (h : ∃ (x : α), x ∈ l ∧ p x = true) : { x : α // x ∈ l ∧ p x = true }

findExisting p l h returns the first element for which p returns true, and attaches membership and predicate p to element