Theorem: Lean4Lean.VExpr.LevelWF.instL (Lean4Lean/Theory/VExpr.lean)

State before:
ls : List VLevel
e : VExpr
U : Nat
h : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
⊢ LevelWF U (VExpr.instL ls e)
Tactic:
induction e <;> simp [instL, VLevel.WF.inst h, LevelWF, *]
State after:
no goals