∀ {α : Sort u_4} {β : Sort u_5} {r : α → α → Prop},
  WellFounded r →
    ∀ {a bot : α} {C : β → Prop} {f : α → β},
      (∀ (b : α), f b ≠ f bot → C (f b) → ∃ c, r c b ∧ C (f c)) → C (f a) → C (f bot)