right
case intro.intro
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ y = x ∨ ∃ z ∈ ftr f m isDec x, y ∈ f z
case intro.intro.h
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
i : ℕ
IH : ∀ {x y : α}, y ∈ (fun X => (List.map f X).join)^[i] [x] → y ∈ ftr f m isDec x
x y b : α
b_in_fiX : b ∈ (fun X => (List.map f X).join)^[i] [x]
y_in_fb : y ∈ f b
⊢ ∃ z ∈ ftr f m isDec x, y ∈ f z