no goals
α : Type u_1
β : Type ?u.157987
γ : Type ?u.157990
δ : Type ?u.157993
σ : Type ?u.157996
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
f : α → ℕ
p : α → ℕ → Prop
inst✝ : (x : α) → (n : ℕ) → Decidable (p x n)
hf : Primrec f
hp : PrimrecRel p
x : α
⊢ Nat.rec 0 (fun n IH => if p x ((n, IH).fst + 1) then (n, IH).fst + 1 else (n, IH).snd) (f x) =
    Nat.findGreatest (p x) (f x)
induction f x <;> simp [Nat.findGreatest, *]