Theorem: Lean4Lean.VExpr.instL_instL (Lean4Lean/Theory/VExpr.lean)

State before:
ls ls' : List VLevel
e : VExpr
⊢ instL ls' (instL ls e) = instL (List.map (VLevel.inst ls') ls) e
Tactic:
cases e <;> simp [instL, instL_instL, Function.comp_def, VLevel.inst_inst]
State after:
no goals