case inr hyp =>
  right
  rcases hyp with ⟨a, a_in_x, y_in_ftr_a⟩
  rw [ftr.iff'] at y_in_ftr_a cases y_in_ftr_a
  case inl y_is_a =>
    subst y_is_a
    use x
    unfold ftr
    aesop
  case inr hyp =>
    rcases hyp with ⟨z, z_in_ftr_a, y_in_fz⟩
    use z
    rw [ftr.iff]
    aesop
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
hyp : ∃ a ∈ f x, y ∈ ftr f m isDec a
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
no goals