use x
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a_in_x : y ∈ f x
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a_in_x : y ∈ f x
⊢ x ∈ ftr f m isDec x ∧ y ∈ f x