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

State before:
u : Nat
l : VLevel
h : WF u l
⊢ inst (List.map param (List.range u)) l = l
Tactic:
induction l <;> simp_all [inst, WF, List.getD_eq_get?, List.get?_range]
State after:
no goals