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

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