simp[elimL, decode_eq, Function.comp, SubWType.elimDecode, SubWType.elim']
α : 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
      (elim γ fun x =>
        match x with
        | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
      (decode e) =
    SubWType.elimDecode β f e.unpair.1 e.unpair.2
α : 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)