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

State before:
e : VExpr
k : Nat
⊢ instVar 0 e (k + 1) = bvar 0
Tactic:
simp [instVar]
State after:
no goals