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

State before:
i : Nat
e : VExpr
k : Nat
ls : List VLevel
⊢ instL ls (instVar i e k) = instVar i (instL ls e) k
Tactic:
simp [instVar]
State after:
i : Nat
e : VExpr
k : Nat
ls : List VLevel
⊢ instL ls (if i < k then bvar i else if i = k then liftN k e else bvar (i - 1)) =
    if i < k then bvar i else if i = k then liftN k (instL ls e) else bvar (i - 1)

State before:
i : Nat
e : VExpr
k : Nat
ls : List VLevel
⊢ instL ls (if i < k then bvar i else if i = k then liftN k e else bvar (i - 1)) =
    if i < k then bvar i else if i = k then liftN k (instL ls e) else bvar (i - 1)
Tactic:
split <;> [skip; split] <;> simp [instL, instL_liftN]
State after:
no goals