no goals
α : Type ?u.360281
β : Type ?u.360284
γ : Type ?u.360287
σ : Type ?u.360290
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Primrec fun a => ↑(Fin.succ a)
simp [succ.comp fin_val]