n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ g
      (abs
        { fst := a,
          snd :=
            splitFun f' fun i =>
              MvPFunctor.wRec (P F) (fun a f' _f rec => g (abs { fst := a, snd := splitFun f' rec })) (f i) }) =
    g
      (abs
        { fst := a,
          snd :=
            splitFun f' ((MvPFunctor.wRec (P F) fun a f' _f rec => g (abs { fst := a, snd := splitFun f' rec })) ∘ f) })
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ recF g (MvPFunctor.wMk (P F) a f' f) = g (abs { fst := a, snd := splitFun f' (recF g ∘ f) })
rw [recF, MvPFunctor.wRec_eq]
no goals
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ g
      (abs
        { fst := a,
          snd :=
            splitFun f' fun i =>
              MvPFunctor.wRec (P F) (fun a f' _f rec => g (abs { fst := a, snd := splitFun f' rec })) (f i) }) =
    g
      (abs
        { fst := a,
          snd :=
            splitFun f' ((MvPFunctor.wRec (P F) fun a f' _f rec => g (abs { fst := a, snd := splitFun f' rec })) ∘ f) })
rfl