case a.h
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
h : WPath P (WType.mk a f) ⟹ α
i : Fin2 n
x : WPath P (WType.mk a fun j => f j) i
⊢ wPathCasesOn P (wPathDestLeft P h) (wPathDestRight P h) i x = h i x
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
h : WPath P (WType.mk a f) ⟹ α
⊢ wPathCasesOn P (wPathDestLeft P h) (wPathDestRight P h) = h
ext (i x)
no goals
case a.h
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a : P.A
f : PFunctor.B (last P) a → PFunctor.W (last P)
h : WPath P (WType.mk a f) ⟹ α
i : Fin2 n
x : WPath P (WType.mk a fun j => f j) i
⊢ wPathCasesOn P (wPathDestLeft P h) (wPathDestRight P h) i x = h i x
cases x <;> rfl