no goals
α✝ : Type ?u.19256
β✝ : Type ?u.19259
σ : Type ?u.19262
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Primcodable β
f : α → β
h : Primrec f
n : ℕ
⊢ Nat.pred (encode (Option.map f (decode n))) = encode (f (ofNat α n))
simp
no goals
α✝ : Type ?u.19256
β✝ : Type ?u.19259
σ : Type ?u.19262
inst✝⁴ : Primcodable α✝
inst✝³ : Primcodable β✝
inst✝² : Primcodable σ
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Primcodable β
f : α → β
h : Nat.Primrec fun n => encode (f (ofNat α n))
n : ℕ
⊢ Nat.succ (encode (f (ofNat α n))) = encode (Option.map f (decode n))
simp