case a.h
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
i : Fin2 n
x✝ : drop (Subtype_ p) i
⊢ dropFun (ofSubtype p) i x✝ = ofSubtype (dropFun p) i x✝
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
⊢ dropFun (ofSubtype p) = ofSubtype (dropFun p)
ext i : 2
no goals
case a.h
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
i : Fin2 n
x✝ : drop (Subtype_ p) i
⊢ dropFun (ofSubtype p) i x✝ = ofSubtype (dropFun p) i x✝
induction i <;> simp [dropFun, *] <;> rfl