n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ (MvPFunctor.wMk' (P F) ∘ repr)
      (abs ((TypeVec.id ::: recF (MvPFunctor.wMk' (P F) ∘ repr)) <$$> { fst := a, snd := splitFun f' f })) =
    MvPFunctor.wMk' (P F)
      (repr
        (abs
          ((TypeVec.id ::: recF (MvPFunctor.wMk' (P F) ∘ repr)) <$$>
            { fst := a, snd := MvPFunctor.appendContents (P F) f' f })))
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ wrepr (MvPFunctor.wMk (P F) a f' f) =
    MvPFunctor.wMk' (P F)
      (repr (abs ((TypeVec.id ::: wrepr) <$$> { fst := a, snd := MvPFunctor.appendContents (P F) f' f })))
rw [wrepr, recF_eq', q.P.wDest'_wMk]
no goals
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
a : (P F).A
f' : MvPFunctor.B (MvPFunctor.drop (P F)) a ⟹ α
f : PFunctor.B (MvPFunctor.last (P F)) a → MvPFunctor.W (P F) α
⊢ (MvPFunctor.wMk' (P F) ∘ repr)
      (abs ((TypeVec.id ::: recF (MvPFunctor.wMk' (P F) ∘ repr)) <$$> { fst := a, snd := splitFun f' f })) =
    MvPFunctor.wMk' (P F)
      (repr
        (abs
          ((TypeVec.id ::: recF (MvPFunctor.wMk' (P F) ∘ repr)) <$$>
            { fst := a, snd := MvPFunctor.appendContents (P F) f' f })))
rfl