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

State before:
n i k i' : Nat
⊢ liftVar n i k = liftVar n i' k ↔ i = i'
Tactic:
simpa [liftN] using @liftN_inj n (.bvar i) k (.bvar i')
State after:
no goals