no goals
α : Type u_2
β : Type u_1
γ : Type ?u.111139
δ : Type ?u.111142
σ : Type u_3
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ (Nat.casesOn (encode (o a)) (encode (f a)) fun b =>
      Nat.pred (encode (Option.bind (decode (encode (a, b).fst)) fun a => Option.map (g a) (decode b)))) =
    encode (Option.casesOn (o a) (f a) (g a))
cases' o a with b <;> simp [encodek]