Theorem: Qq.compVecEmpty (Logic/Vorspiel/Meta.lean)

State before:
α : Type u
β : Type v
f : α → β
⊢ f ∘ ![] = ![]
Tactic:
simp
State after:
no goals