case h
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
i : last (Subtype_ p)
⊢ lastFun (ofSubtype p) i = _root_.id i
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
⊢ lastFun (ofSubtype p) = _root_.id
ext i : 2
case h.mk
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
val✝ : α Fin2.fz
property✝ : p Fin2.fz val✝
⊢ lastFun (ofSubtype p) { val := val✝, property := property✝ } = _root_.id { val := val✝, property := property✝ }
case h
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
i : last (Subtype_ p)
⊢ lastFun (ofSubtype p) i = _root_.id i
induction i
case h.mk
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
val✝ : α Fin2.fz
property✝ : p Fin2.fz val✝
⊢ lastFun (ofSubtype p) { val := val✝, property := property✝ } = { val := val✝, property := property✝ }
case h.mk
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
val✝ : α Fin2.fz
property✝ : p Fin2.fz val✝
⊢ lastFun (ofSubtype p) { val := val✝, property := property✝ } = _root_.id { val := val✝, property := property✝ }
simp [dropFun, *]
no goals
case h.mk
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
val✝ : α Fin2.fz
property✝ : p Fin2.fz val✝
⊢ lastFun (ofSubtype p) { val := val✝, property := property✝ } = { val := val✝, property := property✝ }
rfl