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

State before:
n : Nat
e : VExpr
k : Nat
ls : List VLevel
⊢ instL ls (liftN n e k) = liftN n (instL ls e) k
Tactic:
cases e <;> simp [liftN, instL, instL_liftN]
State after:
no goals