induction i
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
⊢ ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
case zero
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[0] [x] → y ∈ ftr f m isDec x

case succ
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
n✝ : ℕ
a✝ : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[n✝] [x] → y ∈ ftr f m isDec x
⊢ ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[n✝ + 1] [x] → y ∈ ftr f m isDec x