[GOAL]
n : ℕ
i : Fin2 n
⊢ ∀ {α : TypeVec n} (x : Prj i α), abs i (repr i x) = x
[PROOFSTEP]
intros
[GOAL]
n : ℕ
i : Fin2 n
α✝ : TypeVec n
x✝ : Prj i α✝
⊢ abs i (repr i x✝) = x✝
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
i : Fin2 n
⊢ ∀ {α β : TypeVec n} (f : α ⟹ β) (p : MvPFunctor.Obj (P i) α), abs i (f <$$> p) = f <$$> abs i p
[PROOFSTEP]
intros α β f P
[GOAL]
n : ℕ
i : Fin2 n
α β : TypeVec n
f : α ⟹ β
P : MvPFunctor.Obj (MvQPF.Prj.P i) α
⊢ abs i (f <$$> P) = f <$$> abs i P
[PROOFSTEP]
cases P
[GOAL]
case mk
n : ℕ
i : Fin2 n
α β : TypeVec n
f : α ⟹ β
fst✝ : (P i).A
snd✝ : MvPFunctor.B (P i) fst✝ ⟹ α
⊢ abs i (f <$$> { fst := fst✝, snd := snd✝ }) = f <$$> abs i { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
