simp[Encodable.decode_sigma_val, Option.map_bind', Function.comp]
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯) (decode e) =
    (decode e.unpair.1).bind fun a =>
      Option.map (fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯) (decode e.unpair.2)
no goals