unfold ftr
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
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 ∈
      let x := x;
      [x] ++
        (List.map
            (fun x_1 =>
              match x_1 with
              | ⟨y, y_in⟩ =>
                let_fun this := y_in;
                ftr f m isDec y)
            (f x).attach).join) ∧
    y ∈ f x