Theorem: Primrec₂.decode_iff₁ (Logic/Vorspiel/Computability.lean)

State before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → β → σ
h : Primrec₂ fun n b => Option.map (fun x => f x b) (decode n)
⊢ ∀ (a : α) (b : β), Option.map (fun x => f x b) (decode (encode a)) = some (f a b)
Tactic:
simp
State after:
no goals