case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : B P a ⟹ α ::: W P α
⊢ wDest' P (wMk' P { fst := a, snd := f }) = { fst := a, snd := f }
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
x : Obj P (α ::: W P α)
⊢ wDest' P (wMk' P x) = x
cases' x with a f
no goals
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : B P a ⟹ α ::: W P α
⊢ wDest' P (wMk' P { fst := a, snd := f }) = { fst := a, snd := f }
rw [wMk', wDest'_wMk, split_dropFun_lastFun]