rcases (decode e.unpair.2) with (_ | ⟨_, _⟩) <;> simp[SubWType.toW]
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
γ : Type u_3
e : ℕ
f : α → List γ → γ
⊢ Option.map
      (fun x => elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (SubWType.toW ⟨e.unpair.1, x⟩))
      (decode e.unpair.2) =
    Option.map (SubWType.elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) e.unpair.1)
      (decode e.unpair.2)
no goals