apply And.intro
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ (fun n => f^[n] a) 0 = a ∧ ∀ (n : ℕ), Q ((fun n => f^[n] a) n) ((fun n => f^[n] a) (n + 1))
case left
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ (fun n => f^[n] a) 0 = a

case right
A✝ : Type
R : A✝ → A✝ → Prop
inhabited_A : Nonempty A✝
A : Sort u_1
Q : A → A → Prop
a : A
forall_exists_Q : ∀ (a : A), ∃ b, Q a b
choice_aut : ∃ f, ∀ (x : A), Q x (f x)
f : A → A
h : (fun f => ∀ (x : A), Q x (f x)) f
⊢ ∀ (n : ℕ), Q ((fun n => f^[n] a) n) ((fun n => f^[n] a) (n + 1))