theorem exists_by_induction {α : Type u_1} {P : ℕ → α → Prop} (h₀ : ∃ (a : α), P 0 a) (ih : ∀ (n : ℕ) (a : α), P n a → ∃ (a' : α), P (n + 1) a') : ∃ (f : ℕ → α), ∀ (n : ℕ), P n (f n)

theorem exists_by_induction' {α : Type u_1} (P : ℕ → α → Prop) (Q : ℕ → α → α → Prop) (h₀ : ∃ (a : α), P 0 a) (ih : ∀ (n : ℕ) (a : α), P n a → ∃ (a' : α), P (n + 1) a' ∧ Q n a a') : ∃ (f : ℕ → α), ∀ (n : ℕ), P n (f n) ∧ Q n (f n) (f (n + 1))