n : ℕ
α : TypeVec n
β : TypeVec n
p : α ⟹ repeat n Prop
f : β ⟹ Subtype_ p
⊢ id ⊚ f = f
n : ℕ
α : TypeVec n
β : TypeVec n
p : α ⟹ repeat n Prop
f : β ⟹ Subtype_ p
⊢ toSubtype p ⊚ (ofSubtype fun i x => p i x) ⊚ f = f
rw [← comp_assoc, toSubtype_of_subtype]
no goals
n : ℕ
α : TypeVec n
β : TypeVec n
p : α ⟹ repeat n Prop
f : β ⟹ Subtype_ p
⊢ id ⊚ f = f
simp