unfold ftr
α : Type
y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
⊢ y ∈
    let x := a;
    [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
α : Type
y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
y_in_fa : y ∈ f a
⊢ y ∈
    let x := a;
    [x] ++
      (List.map
          (fun x_1 =>
            let x := ↑x_1;
            [x] ++
              (List.map
                  (fun x_2 =>
                    match x_2 with
                    | ⟨y, y_in⟩ =>
                      let_fun this := y_in;
                      ftr f m isDec y)
                  (f x).attach).join)
          (f x).attach).join