Theorem: Lean4Lean.VExpr.inst_liftN' (Lean4Lean/Theory/VExpr.lean)

State before:
n k : Nat
e1 e2 : VExpr
⊢ inst (liftN (n + 1) e1 k) e2 k = liftN n e1 k
Tactic:
rw [← liftN'_liftN_hi, inst_liftN]
State after:
no goals