n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : MvPFunctor.W (P 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 ((TypeVec.id ::: recF g) <$$> MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a f' f)))
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : MvPFunctor.W (P F) α
⊢ recF g x = g (abs ((TypeVec.id ::: recF g) <$$> MvPFunctor.wDest' (P F) x))
apply q.P.w_cases _ x
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : MvPFunctor.W (P 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 ((TypeVec.id ::: recF g) <$$> MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a f' f)))
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : MvPFunctor.W (P 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 ((TypeVec.id ::: recF g) <$$> MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a f' f)))
intro a f' f
no goals
n : ℕ
F : TypeVec (n + 1) → Type u
inst✝ : MvFunctor F
q : MvQPF F
α : TypeVec n
β : Type u
g : F (α ::: β) → β
x : MvPFunctor.W (P 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 ((TypeVec.id ::: recF g) <$$> MvPFunctor.wDest' (P F) (MvPFunctor.wMk (P F) a f' f)))
rw [recF_eq, q.P.wDest'_wMk, MvPFunctor.map_eq, appendFun_comp_splitFun, TypeVec.id_comp]