simp[inversion, Function.comp, elimvL_mk]
case mk.mk.mk
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
z : τ
x : σ
a : α
f : β a → WType β
⊢ some
      (fγ (z, x, WType.mk a f).1
        ((z, x, WType.mk a f).2.1, (z, x, WType.mk a f).2.2.inversion.1,
          List.map (fun p => elimvL (fun a x => fs p.1 (a, x)) (fun x a l => fγ p.1 (x, a, l)) p.2.1 p.2.2)
            (List.map
              (fun w =>
                ((z, x, WType.mk a f).1,
                  fs (z, x, WType.mk a f).1 ((z, x, WType.mk a f).2.2.inversion.1, (z, x, WType.mk a f).2.1), w))
              (z, x, WType.mk a f).2.2.inversion.2))) =
    some
      (elimvL (fun a_1 x_1 => fs (z, x, WType.mk a f).1 (a_1, x_1))
        (fun x_1 a_1 l => fγ (z, x, WType.mk a f).1 (x_1, a_1, l)) (z, x, WType.mk a f).2.1 (z, x, WType.mk a f).2.2)
case mk.mk.mk
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
z : τ
x : σ
a : α
f : β a → WType β
⊢ fγ z
      (x, a,
        List.ofFn fun x_1 =>
          elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (fs z (a, x)) (f (fintypeEquivFin.symm x_1))) =
    fγ z
      (x, a,
        List.ofFn
          (fintypeArrowEquivFinArrow fun b =>
            elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (fs z (a, x)) (f b)))