case mk
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
f : α ⟹ β
fst✝ : (const n A).A
snd✝ : B (const n A) fst✝ ⟹ α
⊢ get (f <$$> { fst := fst✝, snd := snd✝ }) = get { fst := fst✝, snd := snd✝ }
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
f : α ⟹ β
x : Obj (const n A) α
⊢ get (f <$$> x) = get x
cases x
no goals
case mk
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
f : α ⟹ β
fst✝ : (const n A).A
snd✝ : B (const n A) fst✝ ⟹ α
⊢ get (f <$$> { fst := fst✝, snd := snd✝ }) = get { fst := fst✝, snd := snd✝ }
rfl