simp[Option.map_bind']
case e_a.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
a : α
⊢ Option.map (fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯)
      ((decode e.unpair.2).bind fun l =>
        Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card (β a)) l)) =
    (decode e.unpair.2).bind fun l =>
      Option.map (fun v => ofWType (WType.mk a fun b => ↑(fintypeArrowEquivVector.symm v b)) (s + 1) ⋯)
        (List.toVector (Fintype.card (β a)) l)
case e_a.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
a : α
⊢ ((decode e.unpair.2).bind fun a_1 =>
      Option.map ((fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯) ∘ ⇑fintypeArrowEquivVector.symm)
        (List.toVector (Fintype.card (β a)) a_1)) =
    (decode e.unpair.2).bind fun a_1 =>
      Option.map (fun v => ofWType (WType.mk a fun b => ↑(v.get (fintypeEquivFin b))) (s + 1) ⋯)
        (List.toVector (Fintype.card (β a)) a_1)