Theorem: MvQPF.Arrow.unbox_box_id (Qpf/PFunctor/Multivariate/Constructions/Arrow.lean)

State before:
α : Type
Γ : TypeVec.{0} 1
f : Arrow' α Γ
⊢ unbox (box f) = f
Tactic:
rfl
State after:
no goals