case mk
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
fst✝ : (const n A).A
snd✝ : B (const n A) fst✝ ⟹ α
⊢ mk n (get { fst := fst✝, snd := snd✝ }) = { fst := fst✝, snd := snd✝ }
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
x : Obj (const n A) α
⊢ mk n (get x) = x
cases x
case mk
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
fst✝ : (const n A).A
snd✝ : B (const n A) fst✝ ⟹ α
⊢ { fst := fst✝, snd := fun x a => PEmpty.elim a } = { fst := fst✝, snd := snd✝ }
case mk
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
fst✝ : (const n A).A
snd✝ : B (const n A) fst✝ ⟹ α
⊢ mk n (get { fst := fst✝, snd := snd✝ }) = { fst := fst✝, snd := snd✝ }
dsimp [const.get, const.mk]
no goals
case mk
n m : ℕ
P : MvPFunctor n
A : Type u
α β : TypeVec n
fst✝ : (const n A).A
snd✝ : B (const n A) fst✝ ⟹ α
⊢ { fst := fst✝, snd := fun x a => PEmpty.elim a } = { fst := fst✝, snd := snd✝ }
congr with (_⟨⟩)