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

State before:
n : Nat
e : VExpr
k : Nat
⊢ unliftN (liftN n e k) n k = e
Tactic:
induction n <;> simp [unliftN, inst_liftN', *]
State after:
no goals