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

State before:
e : VExpr
k : Nat
⊢ inst (liftN 1 e (k + 1)) (bvar 0) k = e
Tactic:
induction e generalizing k with simp [liftN, inst, *]
| bvar i => induction i generalizing k <;> cases k <;> simp [*, lift, liftN]
State after:
no goals

State before:
case bvar
i k : Nat
⊢ instVar (liftVar 1 i (k + 1)) (bvar 0) k = bvar i
Tactic:
induction i generalizing k <;> cases k <;> simp [*, lift, liftN]
State after:
no goals