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

State before:
n : Nat
e1 : VExpr
k : Nat
e2 : VExpr
H : liftN n e1 k = liftN n e2 k
⊢ e1 = e2
Tactic:
rw [← unliftN_liftN (e := e1), H, unliftN_liftN]
State after:
no goals