Theorem: Lean4Lean.VLevel.id_WF (Lean4Lean/Theory/VLevel.lean)

State before:
u : Nat
⊢ ∀ (l : VLevel), l ∈ List.map param (List.range u) → WF u l
Tactic:
simp [WF]
State after:
no goals