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

State before:
k : Nat
ls : List VLevel
e1 e2 : VExpr
⊢ instL ls (inst e1 e2 k) = inst (instL ls e1) (instL ls e2) k
Tactic:
induction e1 generalizing k <;> simp [instL, inst, *]
State after:
no goals