cases y_in_ftr_a
case h.intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
y_in_ftr_a : y = a ∨ ∃ z ∈ ftr f m isDec a, y ∈ f z
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z
case h.intro.intro.inl
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
h✝ : y = a
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z

case h.intro.intro.inr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
h✝ : ∃ z ∈ ftr f m isDec a, y ∈ f z
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z