constructor
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ y ∈ ftr f m isDec x ↔ y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z
case mp
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ y ∈ ftr f m isDec x → y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z

case mpr
α : Type
x y : α
f : α → List α
m : α → ℕ
isDec : ∀ (x y : α), y ∈ f x → m y < m x
⊢ (y = x ∨ ∃ z ∈ f x, y ∈ ftr f m isDec z) → y ∈ ftr f m isDec x