Theorem: Lean4Lean.VExpr.ClosedN.instN_eq (Lean4Lean/Theory/VExpr.lean)

State before:
e1 : VExpr
k j : Nat
e2 : VExpr
self : ClosedN e1 k
h : k ≤ j
⊢ inst e1 e2 j = e1
Tactic:
conv => lhs; rw [← self.liftN_eq (n := 1) h]
State after:
e1 : VExpr
k j : Nat
e2 : VExpr
self : ClosedN e1 k
h : k ≤ j
⊢ inst (liftN 1 e1 j) e2 j = e1

State before:
e1 : VExpr
k j : Nat
e2 : VExpr
self : ClosedN e1 k
h : k ≤ j
⊢ inst (liftN 1 e1 j) e2 j = e1
Tactic:
rw [inst_liftN]
State after:
no goals