have h : ∃ (f : ℕ → {x : A // P x}), f 0 = ⟨a, pa⟩
         ∧ ∀ n, P (f n) ∧ Q (f n) (f (n+1)) :=
by
  apply (@dependent_choice' {x : A // P x} (λ p q => P p ∧ Q p q) _)
  intros ap
  match ap with
  | Subtype.mk a' p =>
    simp
    apply And.intro
    . exact p
    . match (ex a' p) with
      | Exists.intro b ⟨pb, qb⟩ => exists (Subtype.mk b pb)
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
⊢ ∃ f, f 0 = a ∧ ∀ (n : ℕ), P (f n) ∧ Q (f n) (f (n + 1))
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
Q : A → A → Prop
a : A
pa : P a
ex : ∀ (a : A), P a → ∃ b, P b ∧ Q a b
h : ∃ f, f 0 = { val := a, property := pa } ∧ ∀ (n : ℕ), P (f n).val ∧ Q (f n).val (f (n + 1)).val
⊢ ∃ f, f 0 = a ∧ ∀ (n : ℕ), P (f n) ∧ Q (f n) (f (n + 1))