{ simp[encodeDecode_eq_encode_map_decode, Function.comp] }
case some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
a : α
⊢ Option.map (fun x => a) (encodeDecode (β a) n.unpair.2) = Option.map (Sigma.fst ∘ Sigma.mk a) (decode n.unpair.2)
no goals