aesop
case h
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
a : α
a_in_x : a ∈ f x
z : α
z_in_ftr_a : z ∈ ftr f m isDec a
y_in_fz : y ∈ f z
⊢ (z = x ∨ ∃ z_1 ∈ f x, z ∈ ftr f m isDec z_1) ∧ y ∈ f z
no goals