have y_in_ftr_z : y ∈ ftr f m isDec z := by
  rw [ftr.iff']
  right
  use a
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
z : α
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec x
case intro.intro
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
z : α
z_in_fx : z ∈ f x
a_in_ftr_z : a ∈ ftr f m isDec z
y_in_ftr_z : y ∈ ftr f m isDec z
⊢ y ∈ ftr f m isDec x