simp
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
k : ℕ
IH :
  ∀ m_1 < k, ∀ {x : α} {x_1 : m_1 = m x} {y : α}, y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
x : α
k_is : k = m x
y z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ [z] ⊆ f x
α : Type
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
k : ℕ
IH :
  ∀ m_1 < k, ∀ {x : α} {x_1 : m_1 = m x} {y : α}, y ∈ ftr f m isDec x → ∃ i, y ∈ (fun X => (List.map f X).join)^[i] [x]
x : α
k_is : k = m x
y z : α
z_in_fx : z ∈ f x
y_in_ftr_z : y ∈ ftr f m isDec z
j : ℕ
y_in : y ∈ (fun X => (List.map f X).join)^[j] [z]
⊢ z ∈ f x